From 0b057a6f3f1b803c387d3fcef714f801d42225b2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Jan 2006 18:23:43 +0000
Subject: [PATCH] Pigeonhole proof restructured.

---
 helm/matita/library/algebra/groups.ma | 100 +++++++++++++-------------
 1 file changed, 52 insertions(+), 48 deletions(-)

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index bea22afc0..4fcca3499 100644
--- 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
     ]
   ]
 ].
-- 
2.39.5