Pigeonhole proof restructured.

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index bea22afc048824e1ffbc6ef63ca61b1e7777edde..4fcca34993cd060e7a473e3a211e0f3c2e2935f7 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -309,30 +309,61 @@ elim n;
         [ true ⇒ pred fx
         | false ⇒ fx
         ]);
-    elim (H f' ? ? x);
-    [ simplify in H5;
-      clear f';
-      elim H5;
-      clear H5;
-      apply (ex_intro ? ? a);
-      split;
-      [ generalize in match H4;
-        clear H4;
-        rewrite < H6;
-        clear H6;
-        apply (ltb_elim (f (S n1)) (f a));
-        [ (* TODO: caso impossibile (uso l'iniettivita') *)
-          simplify;
-        | simplify;
-          intros;
-          reflexivity
-        ]        
-      | apply le_S;
+    cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+    [ elim (H f' ? ? x);
+      [ simplify in H5;
+        clear Hcut;
+        clear f';
+        elim H5;
+        clear H5;
+        apply (ex_intro ? ? a);
+        split;
+        [ generalize in match H4;
+          clear H4;
+          rewrite < H6;
+          clear H6;
+          apply (ltb_elim (f (S n1)) (f a));
+          [ (* TODO: caso impossibile (uso l'iniettivita') *)
+            simplify;
+          | simplify;
+            intros;
+            reflexivity
+          ]        
+        | apply le_S;
+          assumption
+        ]
+      | apply Hcut    
+      | simplify;
+        intro;
+        apply (ltb_elim (f (S n1)) (f m));
+        simplify;
+        intro;
+        [ generalize in match (H2 m);
+          intro;
+          change in match n1 with (pred (S n1));
+          apply le_to_le_pred;
+          assumption
+        | generalize in match (H2 (S n1));
+          intro;
+          generalize in match (not_lt_to_le ? ? H5);
+          intro;
+          generalize in match (transitive_le ? ? ? H7 H6);
+          intro;
+          (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *) 
+        ]
+      | rewrite > (pred_Sn n1);
+        simplify;
+        generalize in match (H2 (S n1));
+        intro;
+        generalize in match (lt_to_le_to_lt ? ? ? H4 H5);
+        intro;
+        unfold lt in H6;
+        apply le_S_S_to_le;
         assumption
       ]
-    | (* This branch proves injectivity of f' *)    
+    | intros 4;
+      unfold f';
       simplify;
-      intros 4;
       apply (ltb_elim (f (S n1)) (f x1));
       simplify;
       apply (ltb_elim (f (S n1)) (f y));
@@ -412,33 +443,6 @@ elim n;
         apply le_S;
         assumption
       ]
-    | simplify;
-      intro;
-      apply (ltb_elim (f (S n1)) (f m));
-      simplify;
-      intro;
-      [ generalize in match (H2 m);
-        intro;
-        change in match n1 with (pred (S n1));
-        apply le_to_le_pred;
-        assumption
-      | generalize in match (H2 (S n1));
-        intro;
-        generalize in match (not_lt_to_le ? ? H5);
-        intro;
-        generalize in match (transitive_le ? ? ? H7 H6);
-        intro;
-        (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *) 
-      ]
-    | rewrite > (pred_Sn n1);
-      simplify;
-      generalize in match (H2 (S n1));
-      intro;
-      generalize in match (lt_to_le_to_lt ? ? ? H4 H5);
-      intro;
-      unfold lt in H6;
-      apply le_S_S_to_le;
-      assumption
     ]
   ]
 ].