+\def monotonic_le_times_l. *)
+
+ntheorem le_times: ∀n1,n2,m1,m2:nat.
+n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2.
+#n1; #n2; #m1; #m2; #len; #lem;
+napply transitive_le; (* /2/ slow *)
+ ##[ ##| napply monotonic_le_times_l;//;
+ ##| napply monotonic_le_times_r;//;
+ ##]
+nqed.
+
+ntheorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
+(* bello *)
+/2/; nqed.
+
+ntheorem le_times_to_le:
+∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
+#a; napply nat_elim2; nnormalize;
+ ##[//;
+ ##|#n; #H1; #H2; napply False_ind;
+ ngeneralize in match H2;
+ napply lt_to_not_le;
+ napply (transitive_le ? (S n));/2/;
+ ##|#n; #m; #H; #lta; #le;
+ napply le_S_S; napply H; /2/;
+ ##]
+nqed.
+
+ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → n < 2*m.
+#n; #m; #posm; #lenm; (* interessante *)
+nnormalize; napplyS (le_plus n); //; nqed.
+
+(************************** minus ******************************)
+
+nlet rec minus n m ≝
+ match n with
+ [ O ⇒ O
+ | S p ⇒
+ match m with
+ [ O ⇒ S p
+ | S q ⇒ minus p q ]].
+
+interpretation "natural minus" 'minus x y = (minus x y).
+
+ntheorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+//; nqed.
+
+ntheorem minus_O_n: ∀n:nat.O=O-n.
+#n; ncases n; //; nqed.
+
+ntheorem minus_n_O: ∀n:nat.n=n-O.
+#n; ncases n; //; nqed.
+
+ntheorem minus_n_n: ∀n:nat.O=n-n.
+#n; nelim n; //; nqed.
+
+ntheorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
+#n; nelim n; //; nqed.
+
+ntheorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
+(* qualcosa da capire qui
+#n; #m; #lenm; nelim lenm; napplyS refl_eq. *)
+napply nat_elim2;
+ ##[//
+ ##|#n; #abs; napply False_ind;/2/;
+ ##|/3/;
+ ##]
+nqed.
+
+ntheorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
+napply nat_elim2; //; nqed.
+
+ntheorem plus_minus:
+∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
+napply nat_elim2;
+ ##[//
+ ##|#n; #p; #abs; napply False_ind;/2/;
+ ##|nnormalize;/3/;
+ ##]
+nqed.