New entry: fermat's little theorem (almost complete).

[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 6ff744dcb5a3aa5e8cc626b20ae2740bda00b49c..8302f7ce5873aee8dc6f7893065068e0fb38feb7 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -82,20 +82,22 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
 qed.
 
-theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+theorem plus_to_minus :\forall n,m,p:nat.
 n = m+p \to n-m = p.
 intros.
 apply inj_plus_r m.
-rewrite < H1.
+rewrite < H.
 rewrite < sym_plus.
 symmetry.
-apply plus_minus_m_m.assumption.
+apply plus_minus_m_m.rewrite > H.
+rewrite > sym_plus.
+apply le_plus_n.
 qed.
 
 theorem minus_S_S : \forall n,m:nat.
@@ -118,8 +120,8 @@ intros 2.
 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
@@ -215,24 +217,19 @@ qed.
 theorem distributive_times_minus: distributive nat times minus.
 simplify.
 intros.
-apply (leb_elim z y).intro.
-cut x*(y-z)+x*z = (x*y-x*z)+x*z.
-apply inj_plus_l (x*z).
-assumption.
-apply trans_eq nat ? (x*y).
-rewrite < distr_times_plus. 
-rewrite < plus_minus_m_m ? ? H.reflexivity.
-rewrite < plus_minus_m_m ? ? ?.reflexivity.
-apply le_times_r.
-assumption.
-intro.
-rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (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.
+apply (leb_elim z y).
+  intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+    apply inj_plus_l (x*z).assumption.
+    apply trans_eq nat ? (x*y).
+      rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
+      rewrite < plus_minus_m_m.
+        reflexivity.
+        apply le_times_r.assumption.
+  intro.rewrite > eq_minus_n_m_O.
+    rewrite > eq_minus_n_m_O (x*y).
+      rewrite < sym_times.simplify.reflexivity.
+        apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
+        apply lt_to_le.apply not_le_to_lt.assumption.
 qed.
 
 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
@@ -240,27 +237,23 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 intros.
-cut m+p \le n \or \not m+p \le n.
-elim Hcut.
-apply sym_eq.
-apply plus_to_minus.assumption.
-rewrite > assoc_plus.
-rewrite > sym_plus p.
-rewrite < plus_minus_m_m.
-rewrite > sym_plus.
-rewrite < plus_minus_m_m.reflexivity.
-rewrite > eq_minus_n_m_O n (m+p).
-rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
-apply decidable_le (m+p) n.
-apply le_plus_to_minus_r.
-rewrite > sym_plus.assumption.
-apply trans_le ? (m+p).
-rewrite < sym_plus.
-apply le_plus_n.assumption.
-apply lt_to_le.apply not_le_to_lt.assumption.
-apply le_plus_to_minus.
-apply lt_to_le.apply not_le_to_lt.
-rewrite < sym_plus.assumption.
+cut m+p \le n \or m+p \nleq n.
+  elim Hcut.
+    symmetry.apply plus_to_minus.
+    rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
+      rewrite > sym_plus.rewrite < plus_minus_m_m.
+        reflexivity.
+        apply trans_le ? (m+p).
+          rewrite < sym_plus.apply le_plus_n.
+          assumption.
+      apply le_plus_to_minus_r.rewrite > sym_plus.assumption.   
+    rewrite > eq_minus_n_m_O n (m+p).
+      rewrite > eq_minus_n_m_O (n-m) p.
+        reflexivity.
+      apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
+       apply not_le_to_lt. assumption.
+    apply lt_to_le.apply not_le_to_lt.assumption.          
+  apply decidable_le (m+p) n.
 qed.
 
 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
@@ -268,8 +261,6 @@ p+(n-m) = n-(m-p).
 intros.
 apply sym_eq.
 apply plus_to_minus.
-apply le_plus_to_minus.
-apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
 rewrite < assoc_plus.
 rewrite < plus_minus_m_m.
 rewrite < sym_plus.