(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/euler_theorem".
-
include "nat/map_iter_p.ma".
include "nat/totient.ma".
qed.
*)
-
(*this obvious property is useful because simplify, sometimes,
"simplifies too much", and doesn't allow to obtain this simple result.
*)
]
qed.
-
lemma totient_card: \forall n.
totient n = card n (\lambda i.eqb (gcd i n) (S O)).
intros.