(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/totient".
+set "baseuri" "cic:/matita/library_autobatch/nat/totient".
include "auto/nat/count.ma".
include "auto/nat/chinese_reminder.ma".
intro.
apply (nat_case n)
[ intros.
- auto
+ autobatch
(*simplify.
reflexivity*)
| intros 2.
apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
[ unfold min.
apply le_min_aux_r
- | auto
+ | autobatch
(*unfold lt.
apply (nat_case ((S m)*(S m2)))
[ apply le_n
rewrite > sym_gcd.
rewrite > gcd_mod
[ apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| assumption
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
rewrite > sym_gcd.
rewrite > gcd_mod
[ apply (gcd_times_SO_to_gcd_SO ? ? (S m))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*rewrite > sym_times.
assumption*)
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
apply False_ind.
apply H6.
apply eq_gcd_times_SO
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite < gcd_mod
- [ auto
+ [ autobatch
(*rewrite > H4.
rewrite > sym_gcd.
assumption*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
]
| rewrite < gcd_mod
- [ auto
+ [ autobatch
(*rewrite > H5.
rewrite > sym_gcd.
assumption*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)