reflexivity.
qed.
+(*
theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
totient (n*m) = (totient n)*(totient m).
intro.
rewrite > eq_to_eqb_true.
rewrite > eq_to_eqb_true.
reflexivity.
-rewrite < H4.
\ No newline at end of file
+rewrite < H4.
+*)