Some more work...

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 5cefa0db156a209cc9af9f26f05cf77857b87041..04a00c6f7e4184805e92a2263fd19d8fc4101550 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -230,20 +230,12 @@ qed.
 
 theorem eq_pred_to_eq:
  ∀n,m. O < n → O < m → pred n = pred m → n = m.
-intros 2;
-elim n;
-[ elim (Not_lt_n_n ? H)
-| generalize in match H3;
-  clear H3;
-  generalize in match H2;
-  clear H2;
-  elim m;
-  [ elim (Not_lt_n_n ? H2)
-  | simplify in H4;
-    apply (eq_f ? ? S);
-    assumption
-  ]
-].
+intros;
+generalize in match (eq_f ? ? S ? ? H2);
+intro;
+rewrite < S_pred in H3;
+rewrite < S_pred in H3;
+assumption.
 qed.
 
 theorem le_pred_to_le:
@@ -278,6 +270,40 @@ elim n;
 ].
 qed.
 
+theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
+intros;
+unfold Not;
+intro;
+unfold lt in H;
+unfold lt in H1;
+generalize in match (le_S_S ? ? H);
+intro;
+generalize in match (transitive_le ? ? ? H2 H1);
+intro;
+apply (not_le_Sn_n ? H3).
+qed.
+
+theorem lt_S_S: ∀n,m. n < m → S n < S m.
+intros;
+unfold lt in H;
+apply (le_S_S ? ? H).
+qed.
+
+theorem lt_O_S: ∀n. O < S n.
+intro;
+unfold lt;
+apply le_S_S;
+apply le_O_n.
+qed.
+
+theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
+intros;
+unfold lt in H1;
+generalize in match (le_S_S_to_le ? ? H1);
+intro;
+apply cic:/matita/nat/orders/antisym_le.con;
+assumption.
+qed.
 
 theorem pigeonhole:
  ∀n:nat.∀f:nat→nat.
@@ -296,26 +322,75 @@ elim n;
   | apply le_n
   ]
 | clear n;
-  apply (nat_compare_elim (f (S n1)) x);
-  [ (* TODO: caso complicato, ma simile al terzo *) 
-  | intros;
-    apply (ex_intro ? ? (S n1));
-    split;
-    [ assumption
-    | constructor 1
-    ] 
-  | intro;
-    letin f' ≝
-     (λx.
-       let fSn1 ≝ f (S n1) in
-       let fx ≝ f x in
-        match ltb fSn1 fx with
-        [ true ⇒ pred fx
-        | false ⇒ fx
-        ]);
-    cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
-    [ cut (∀x. x ≤ n1 → f' x ≤ n1);
-      [ elim (H f' ? ? x);
+  letin f' ≝
+   (λx.
+    let fSn1 ≝ f (S n1) in
+     let fx ≝ f x in
+      match ltb fSn1 fx with
+      [ true ⇒ pred fx
+      | false ⇒ fx
+      ]);
+  cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+  [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+    [ apply (nat_compare_elim (f (S n1)) x);
+      [ intro;
+        elim (H f' ? ? (pred x));
+        [ simplify in H5;
+          clear Hcut;
+          clear Hcut1;
+          clear f';
+          elim H5;
+          clear H5;
+          apply (ex_intro ? ? a);
+          split;
+          [ generalize in match (eq_f ? ? S ? ? H6);
+            clear H6;
+            intro;
+            rewrite < S_pred in H5;
+            [ generalize in match H4;
+              clear H4;
+              rewrite < H5;
+              clear H5;
+              apply (ltb_elim (f (S n1)) (f a));
+              [ simplify;
+                intros;
+                rewrite < S_pred;
+                [ reflexivity
+                | apply (ltn_to_ltO ? ? H4)
+                ]
+              | simplify;
+                intros;
+                generalize in match (not_lt_to_le ? ? H4);
+                clear H4;
+                intro;
+                generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
+                intro;
+                generalize in match (H1 ? ? ? ? H4);
+                [ intro;
+                |
+                |
+                ]
+              ]
+            | apply (ltn_to_ltO ? ? H4)
+            ]
+          | apply le_S;
+            assumption
+          ]
+        | apply Hcut
+        | apply Hcut1
+        | apply le_S_S_to_le;
+          rewrite < S_pred;
+          exact H3
+        ]    
+        (* TODO: caso complicato, ma simile al terzo *) 
+      | intros;
+        apply (ex_intro ? ? (S n1));
+        split;
+        [ assumption
+        | constructor 1
+        ] 
+      | intro;
+        elim (H f' ? ? x);
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
@@ -329,8 +404,14 @@ elim n;
             rewrite < H6;
             clear H6;
             apply (ltb_elim (f (S n1)) (f a));
-            [ (* TODO: caso impossibile (uso l'iniettivita') *)
-              simplify;
+            [ simplify;
+              intros;
+              generalize in match (lt_S_S ? ? H5);
+              intro;
+              rewrite < S_pred in H6;
+              [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
+              | apply (ltn_to_ltO ? ? H4)
+              ]
             | simplify;
               intros;
               reflexivity
@@ -350,132 +431,132 @@ elim n;
           apply le_S_S_to_le;
           assumption
         ]
-      | unfold f';
-        simplify;
-        intro;
-        apply (ltb_elim (f (S n1)) (f x1));
-        simplify;
-        intros;
-        [ generalize in match (H2 x1);
-          intro;
-          change in match n1 with (pred (S n1));
-          apply le_to_le_pred;
-          apply H7;
-          apply le_S;
-          assumption
-        | generalize in match (H2 (S n1) (le_n ?));
-          intro;
-          generalize in match (not_lt_to_le ? ? H5);
-          intro;
-          generalize in match (transitive_le ? ? ? H8 H7);
-          intro;
-          cut (f x1 ≠ f (S n1));
-          [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H8);
-            intro;
-            unfold lt in H10;
-            generalize in match (transitive_le ? ? ? H10 H7);
-            intro;
-            apply le_S_S_to_le;
-            assumption
-          | unfold Not;
-            intro;
-            generalize in match (H1 ? ? ? ? H10);
-            [ intro;
-              rewrite > H11 in H6;
-              apply (not_le_Sn_n ? H6)
-            | apply le_S;
-              assumption
-            | apply le_n
-            ]
-          ] 
-        ]
       ]
-    | intros 4;
-      unfold f';
+    | unfold f';
       simplify;
+      intro;
       apply (ltb_elim (f (S n1)) (f x1));
       simplify;
-      apply (ltb_elim (f (S n1)) (f y));
-      simplify;
       intros;
-      [ cut (f x1 = f y);
-        [ apply (H1 ? ? ? ? Hcut);
-          apply le_S;
+      [ generalize in match (H2 x1);
+        intro;
+        change in match n1 with (pred (S n1));
+        apply le_to_le_pred;
+        apply H6;
+        apply le_S;
+        assumption
+      | generalize in match (H2 (S n1) (le_n ?));
+        intro;
+        generalize in match (not_lt_to_le ? ? H4);
+        intro;
+        generalize in match (transitive_le ? ? ? H7 H6);
+        intro;
+        cut (f x1 ≠ f (S n1));
+        [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
+          intro;
+          unfold lt in H9;
+          generalize in match (transitive_le ? ? ? H9 H6);
+          intro;
+          apply le_S_S_to_le;
           assumption
-        | apply eq_pred_to_eq;
-          [ apply (ltn_to_ltO ? ? H8)
-          | apply (ltn_to_ltO ? ? H7)
-          | assumption
+        | unfold Not;
+          intro;
+          generalize in match (H1 ? ? ? ? H9);
+          [ intro;
+            rewrite > H10 in H5;
+            apply (not_le_Sn_n ? H5)
+          | apply le_S;
+            assumption
+          | apply le_n
           ]
-        ]         
-      | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
-           so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
-         cut (y < S n1);
-         [ generalize in match (lt_to_not_eq ? ? Hcut);
-           intro;
-           cut (f y ≠ f (S n1));
-           [ cut (f y < f (S n1));
-             [ rewrite < H9 in Hcut2;
-               unfold lt in Hcut2;
-               unfold lt in H8;
-               generalize in match (le_S_S ? ? Hcut2);
-               intro;
-               generalize in match (transitive_le ? ? ? H11 H8);
-               intros;
-               rewrite < (S_pred (f x1)) in H12;
-                [ elim (not_le_Sn_n ? H12)
-                | fold simplify ((f (S n1)) < (f x1)) in H8;
-                 apply (ltn_to_ltO ? ? H8)
-                ]
-             | apply not_eq_to_le_to_lt;
-               [ assumption
-               | apply not_lt_to_le;
-                 assumption
-               ]
-             ]
-           | unfold Not;
+        ] 
+      ]
+    ]
+  | intros 4;
+    unfold f';
+    simplify;
+    apply (ltb_elim (f (S n1)) (f x1));
+    simplify;
+    apply (ltb_elim (f (S n1)) (f y));
+    simplify;
+    intros;
+    [ cut (f x1 = f y);
+      [ apply (H1 ? ? ? ? Hcut);
+        apply le_S;
+        assumption
+      | apply eq_pred_to_eq;
+        [ apply (ltn_to_ltO ? ? H7)
+        | apply (ltn_to_ltO ? ? H6)
+        | assumption
+        ]
+      ]         
+    | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
+         so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
+       cut (y < S n1);
+       [ generalize in match (lt_to_not_eq ? ? Hcut);
+         intro;
+         cut (f y ≠ f (S n1));
+         [ cut (f y < f (S n1));
+           [ rewrite < H8 in Hcut2;
+             unfold lt in Hcut2;
+             unfold lt in H7;
+             generalize in match (le_S_S ? ? Hcut2);
              intro;
-             apply H10;
-             apply (H1 ? ? ? ? H11);
-             [ apply lt_to_le;
+             generalize in match (transitive_le ? ? ? H10 H7);
+             intros;
+             rewrite < (S_pred (f x1)) in H11;
+              [ elim (not_le_Sn_n ? H11)
+              | fold simplify ((f (S n1)) < (f x1)) in H7;
+                apply (ltn_to_ltO ? ? H7)
+              ]
+           | apply not_eq_to_le_to_lt;
+             [ assumption
+             | apply not_lt_to_le;
                assumption
-             | constructor 1
              ]
            ]
-         | unfold lt;
-           apply le_S_S;
-           assumption
-         ]
-      | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
-           f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
-           injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
-         generalize in match (eq_f ? ? S ? ? H9);
-         intro;
-         rewrite < S_pred in H10;
-         [ rewrite < H10 in H7;
-           generalize in match (not_lt_to_le ? ? H8);
-           intro;
-           unfold lt in H7;
-           generalize in match (le_S_S ? ? H11);
+         | unfold Not;
            intro;
-           generalize in match (antisym_le ? ? H12 H7);
-           intro;
-           generalize in match (inj_S ? ? H13);
-           intro;
-           generalize in match (H1 ? ? ? ? H14);
-           [ intro;
-             rewrite > H15 in H5;
-             elim (not_le_Sn_n ? H5)
-           | apply le_S;
+           apply H9;
+           apply (H1 ? ? ? ? H10);
+           [ apply lt_to_le;
              assumption
-           | apply le_n
+           | constructor 1
            ]
-         | apply (ltn_to_ltO ?? H7) 
          ]
-      | apply (H1 ? ? ? ? H9);
-        apply le_S;
-        assumption
-      ]
+       | unfold lt;
+         apply le_S_S;
+         assumption
+       ]
+    | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
+         f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
+         injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
+       generalize in match (eq_f ? ? S ? ? H8);
+       intro;
+       rewrite < S_pred in H9;
+       [ rewrite < H9 in H6;
+         generalize in match (not_lt_to_le ? ? H7);
+         intro;
+         unfold lt in H6;
+         generalize in match (le_S_S ? ? H10);
+         intro;
+         generalize in match (antisym_le ? ? H11 H6);
+         intro;
+         generalize in match (inj_S ? ? H12);
+         intro;
+         generalize in match (H1 ? ? ? ? H13);
+         [ intro;
+           rewrite > H14 in H4;
+           elim (not_le_Sn_n ? H4)
+         | apply le_S;
+           assumption
+         | apply le_n
+         ]
+       | apply (ltn_to_ltO ? ? H6) 
+       ]
+    | apply (H1 ? ? ? ? H8);
+      apply le_S;
+      assumption
     ]
   ]
 ].