(* *)
(**************************************************************************)
-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.
*)
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)
]
qed.
-
lemma totient_card: \forall n.
totient n = card n (\lambda i.eqb (gcd i n) (S O)).
intros.
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)