X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=5cefa0db156a209cc9af9f26f05cf77857b87041;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=bea22afc048824e1ffbc6ef63ca61b1e7777edde;hpb=4424e9d4f0260f136fc8df7bc71764c5904a34c6;p=helm.git

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index bea22afc0..5cefa0db1 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -282,15 +282,19 @@ qed.
 theorem pigeonhole:
  ∀n:nat.∀f:nat→nat.
   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
-  (∀m. f m ≤ n) →
+  (∀m. m ≤ n → f m ≤ n) →
    ∀x. x≤n \to ∃y.f y = x ∧ y ≤ n.
 intro;
 elim n;
 [ apply (ex_intro ? ? O);
   split;
-  rewrite < (le_n_O_to_eq ? H2);
-  rewrite < (le_n_O_to_eq ? (H1 O));
-  reflexivity
+  [ rewrite < (le_n_O_to_eq ? H2);
+    rewrite < (le_n_O_to_eq ? (H1 O ?));
+    [ reflexivity
+    | apply le_n
+    ]
+  | apply le_n
+  ]
 | clear n;
   apply (nat_compare_elim (f (S n1)) x);
   [ (* TODO: caso complicato, ma simile al terzo *) 
@@ -309,30 +313,86 @@ 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') *)
+    cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+    [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+      [ elim (H f' ? ? x);
+        [ simplify in H5;
+          clear Hcut;
+          clear Hcut1;
+          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    
+        | apply Hcut1
+        | rewrite > (pred_Sn n1);
           simplify;
-        | simplify;
-          intros;
-          reflexivity
-        ]        
-      | apply le_S;
-        assumption
+          generalize in match (H2 (S n1));
+          intro;
+          generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
+          intro;
+          unfold lt in H6;
+          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
+            ]
+          ] 
+        ]
       ]
-    | (* 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));
@@ -403,42 +463,19 @@ elim n;
            generalize in match (inj_S ? ? H13);
            intro;
            generalize in match (H1 ? ? ? ? H14);
-           intro;
-           rewrite > H15 in H5;
-           elim (not_le_Sn_n ? H5)
+           [ intro;
+             rewrite > H15 in H5;
+             elim (not_le_Sn_n ? H5)
+           | apply le_S;
+             assumption
+           | apply le_n
+           ]
          | apply (ltn_to_ltO ?? H7) 
          ]
       | apply (H1 ? ? ? ? H9);
         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
     ]
   ]
 ].