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.
+apply (nat_case n).
intro.simplify.intro.reflexivity.
-intros 2.apply nat_case m1.
+intros 2.apply (nat_case m1).
rewrite < sym_times.
-rewrite < sym_times (totient O).
+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)).
+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))).
+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.
+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).