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)