(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/euler_theorem".
-
include "nat/map_iter_p.ma".
include "nat/totient.ma".
reflexivity
| rewrite > gcd_O_n.
apply not_eq_to_eqb_false.
- apply cic:/matita/nat/nat/not_eq_S.con.
+ apply not_eq_S.
unfold Not.
intro.
cut ( (S n) \le O)
apply (totient_card_aux n2 n2).
reflexivity
| apply not_eq_to_eqb_false.
- apply cic:/matita/nat/nat/not_eq_S.con.
+ apply not_eq_S.
unfold Not.
intro.
cut ( (S n2) \le O)