X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ftotient.ma;h=b4f575a404c15982b04cac19db20c7f3428d6fc5;hb=c3bba4af040f8040e5eae07e70690c52f8c614f8;hp=24c3920ed82571324c2977a7be798b492fbf43e7;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index 24c3920ed..b4f575a40 100644
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -31,72 +31,88 @@ qed.
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intro.
-apply (nat_case n).
-intro.simplify.intro.reflexivity.
-intros 2.apply (nat_case m1).
-rewrite < sym_times.
-rewrite < (sym_times (totient O)).
-simplify.intro.reflexivity.
-intros.
-unfold totient.
-apply (count_times m m2 ? ? ? 
-(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))).
-intros.unfold cr_pair.
-apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
-unfold min.
-apply le_min_aux_r.
-change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
-apply (nat_case ((S m)*(S m2))).apply le_n.
-intro.apply le_n.
-intros.
-generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-intro.elim H3.
-apply H4.
-intros.
-generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-intro.elim H3.
-apply H5.
-intros.
-generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-intro.elim H3.
-apply eqb_elim.
-intro.
-rewrite > eq_to_eqb_true.
-rewrite > eq_to_eqb_true.
-reflexivity.
-rewrite < H4.
-rewrite > sym_gcd.
-rewrite > gcd_mod.
-apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < H5.
-rewrite > sym_gcd.
-rewrite > gcd_mod.
-apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite > sym_times.
-assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-intro.
-apply eqb_elim.
-intro.apply eqb_elim.
-intro.apply False_ind.
-apply H6.
-apply eq_gcd_times_SO.
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < gcd_mod.
-rewrite > H4.
-rewrite > sym_gcd.assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < gcd_mod.
-rewrite > H5.
-rewrite > sym_gcd.assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-intro.reflexivity.
-intro.reflexivity.
+apply (nat_case n)
+  [intros.simplify.reflexivity
+  |intros 2.apply (nat_case m1)
+    [rewrite < sym_times.
+     rewrite < (sym_times (totient O)).
+     simplify.intro.reflexivity.
+     |intros.
+      unfold totient.
+      apply (count_times m m2 ? ? ? 
+             (\lambda b,a. cr_pair (S m) (S m2) a b) 
+             (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
+       [intros.unfold cr_pair.
+        apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
+          [unfold min.
+           apply le_min_aux_r
+          |unfold lt.
+           apply (nat_case ((S m)*(S m2)))
+            [apply le_n|intro.apply le_n]
+          ]
+       |intros.
+        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+        intro.elim H3.
+        apply H4
+       |intros.
+        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+        intro.elim H3.
+        apply H5
+       |intros.
+        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+        intro.elim H3.
+        apply eqb_elim
+          [intro.
+           rewrite > eq_to_eqb_true
+             [rewrite > eq_to_eqb_true
+               [reflexivity
+               |rewrite < H4.
+                rewrite > sym_gcd.
+                rewrite > gcd_mod
+                  [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
+                    [unfold lt.apply le_S_S.apply le_O_n
+                    |unfold lt.apply le_S_S.apply le_O_n
+                    |assumption
+                    ]
+                  |unfold lt.apply le_S_S.apply le_O_n
+                  ]
+               ]           
+            |rewrite < H5.
+             rewrite > sym_gcd.
+             rewrite > gcd_mod
+               [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
+                  [unfold lt.apply le_S_S.apply le_O_n
+                  |unfold lt.apply le_S_S.apply le_O_n
+                  |rewrite > sym_times.assumption
+                  ]
+               |unfold lt.apply le_S_S.apply le_O_n
+               ]
+            ]
+          |intro.
+           apply eqb_elim
+           [intro.apply eqb_elim
+              [intro.apply False_ind.
+               apply H6.
+               apply eq_gcd_times_SO
+                 [unfold lt.apply le_S_S.apply le_O_n.
+                 |unfold lt.apply le_S_S.apply le_O_n.
+                 |rewrite < gcd_mod
+                    [rewrite > H4.
+                     rewrite > sym_gcd.assumption
+                    |unfold lt.apply le_S_S.apply le_O_n
+                    ]
+                 |rewrite < gcd_mod
+                    [rewrite > H5.
+                     rewrite > sym_gcd.assumption
+                    |unfold lt.apply le_S_S.apply le_O_n
+                    ]
+                 ]
+              |intro.reflexivity
+              ]
+           |intro.reflexivity
+           ]
+         ]
+       ]
+     ]
+   ]
 qed.
\ No newline at end of file