Small changes

diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma
index 036167bd04535ad298647ccb3b6097e1d9c7997a..66bc6f8651565e43880cd73bdd222280cca9121f 100644 (file)
--- a/matita/library/nat/gcd.ma
+++ b/matita/library/nat/gcd.ma
@@ -519,10 +519,12 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > distr_times_minus.
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
-          elim H1.rewrite > H6.
-          (* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
+          elim H1.
+          (*
+             rewrite > H6.
+             applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
              reflexivity. *);
-          applyS (witness n ? ? (refl_eq ? ?)) timeout=50.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.

diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index 2c6061e0b80c673158812a259d0e944280d0a8f6..b4f575a404c15982b04cac19db20c7f3428d6fc5 100644 (file)
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -31,71 +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.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.
+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