New version of the library.

[helm.git] / helm / matita / library / nat / minus.ma

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 0091cb9b09b93ace2834862b1b84d64d7bdd219d..b6e7fc5e2c5cb098bddcf1354e5483f4cb99b598 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -12,10 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+
 set "baseuri" "cic:/matita/nat/minus".
 
 include "nat/orders_op.ma".
-include "nat/times.ma".
+include "nat/compare.ma".
 
 let rec minus n m \def 
  match n with 
@@ -96,7 +97,7 @@ symmetry.
 apply plus_minus_m_m.assumption.
 qed.
 
-theorem minus_ge_O: \forall n,m:nat.
+theorem eq_minus_n_m_O: \forall n,m:nat.
 le n m \to eq nat (minus n m) O.
 intros 2.
 apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
@@ -124,36 +125,36 @@ apply plus_le.assumption.
 apply le_n_Sm_elim ? ? H1.
 intros.
 *)
-check distributive.
 
-theorem times_minus_distr: \forall n,m,p:nat.
-eq nat (times n (minus m p)) (minus (times n m) (times n p)).
+theorem distributive_times_minus: distributive nat times minus.
+simplify.
 intros.
-apply (leb_ind p m).intro.
-cut eq nat (plus (times n (minus m p)) (times n p)) (plus (minus (times n m) (times n p)) (times n p)).
-apply plus_injective_right ? ? (times n p).
+apply (leb_elim z y).intro.
+cut eq nat (plus (times x (minus y z)) (times x z)) 
+           (plus (minus (times x y) (times x z)) (times x z)).
+apply inj_plus_l (times x z).
 assumption.
-apply trans_eq nat ? (times n m).
-elim (times_plus_distr ? ? ?).
-elim (minus_plus ? ? H).apply refl_equal.
-elim (minus_plus ? ? ?).apply refl_equal.
-apply times_le_monotony_left.
+apply trans_eq nat ? (times x y).
+rewrite < times_plus_distr. 
+rewrite < plus_minus_m_m ? ? H.reflexivity.
+rewrite < plus_minus_m_m ? ? ?.reflexivity.
+apply le_times_r.
 assumption.
 intro.
-elim sym_eq ? ? ? (minus_ge_O ? ? ?).
-elim sym_eq ? ? ? (minus_ge_O ? ? ?).
-elim (sym_times ? ?).simplify.apply refl_equal.
-simplify.
-apply times_le_monotony_left.
-cut (lt m p) \to (le m p).
-apply Hcut.simplify.apply not_le_lt ? ? H.
-intro.apply lt_le.apply H1.
-cut (lt m p) \to (le m p).
-apply Hcut.simplify.apply not_le_lt ? ? H.
-intro.apply lt_le.apply H1.
+rewrite > eq_minus_n_m_O.
+rewrite > eq_minus_n_m_O (times x y).
+rewrite < sym_times.simplify.reflexivity.
+apply lt_to_le.
+apply not_le_to_lt.assumption.
+apply le_times_r.apply lt_to_le.
+apply not_le_to_lt.assumption.
 qed.
 
-theorem minus_le: \forall n,m:nat. le (minus n m) n.
+theorem distr_times_minus: \forall n,m,p:nat.
+eq nat (times n (minus m p)) (minus (times n m) (times n p))
+\def distributive_times_minus.
+
+theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
 intro.elim n.simplify.apply le_n.
 elim m.simplify.apply le_n.
 simplify.apply le_S.apply H.