Some more work on the proof of the pigeonhole principle.

Really tougher than expected.

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 6deb73bd5cee4e285e4f7d87ae6e7a42b96f60d0..bea22afc048824e1ffbc6ef63ca61b1e7777edde 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -348,10 +348,66 @@ elim n;
           | assumption
           ]
         ]         
-      | (* TODO: pred (f x1) = f y assurdo per iniettivita'
-           poiche' y ≠ S n1 da cui f y ≠ f (S n1) da cui f y < f (S n1) < f x1
-           da cui assurdo pred (f x1) = f y *)
-      | (* TODO: f x1 = pred (f y) assurdo per iniettivita' *)
+      | (* 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;
+             intro;
+             apply H10;
+             apply (H1 ? ? ? ? H11);
+             [ apply 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);
+           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 (ltn_to_ltO ?? H7) 
+         ]
       | apply (H1 ? ? ? ? H9);
         apply le_S;
         assumption