+(* a reformulation of totient using card insted of sigma_p *)
+
+theorem totient_card_aux: \forall n,m: nat.
+m = n \to
+sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O))
+= card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
+intros.
+rewrite < H in \vdash (? ? (? % ? ?) ?).
+rewrite < H in \vdash (? ? ? (? % ?)).
+elim (m)
+[ rewrite > card_Sn.
+ cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
+ [ rewrite > Hcut.
+ simplify in \vdash (? ? ? %).
+ rewrite > true_to_sigma_p_Sn
+ [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
+ [ simplify in \vdash (? ? % ?).
+ reflexivity
+ | rewrite > gcd_O_n.
+ apply not_eq_to_eqb_false.
+ apply cic:/matita/nat/nat/not_eq_S.con.
+ unfold Not.
+ intro.
+ cut ( (S n) \le O)
+ [ apply (not_le_Sn_n n ?).
+ apply (transitive_le (S n) O n ? ?);
+ [ apply (Hcut1)
+ | apply (le_O_n n)
+ ]
+ | rewrite > H1.
+ apply le_n
+ ]
+ ]
+ | assumption
+ ]
+ | apply eq_to_eqb_true.
+ rewrite > gcd_SO_n.
+ reflexivity
+ ]
+| cut ((eqb (gcd (S (S n1)) (S (S n))) (S O)) = true
+ \lor (eqb (gcd (S (S n1)) (S (S n))) (S O)) = false)
+ [ elim Hcut
+ [ rewrite > card_Sn.
+ rewrite > true_to_sigma_p_Sn
+ [ rewrite > H2.
+ simplify in \vdash (? ? ? (? % ?)).
+ apply eq_f.
+ assumption
+ | assumption
+ ]
+ | rewrite > card_Sn.
+ rewrite > false_to_sigma_p_Sn
+ [ rewrite > H2.
+ simplify in \vdash (? ? ? (? % ?)).
+ rewrite > sym_plus.
+ rewrite < plus_n_O.
+ assumption
+ | assumption
+ ]
+ ]
+ | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
+ [ left.
+ reflexivity
+ | right.
+ reflexivity
+ ]
+ ]
+]
+qed.
+
+lemma totient_card: \forall n.
+totient n = card n (\lambda i.eqb (gcd i n) (S O)).
+intros.
+elim n
+[ simplify.
+ reflexivity
+| elim n1
+ [ simplify.
+ reflexivity
+ |
+ (*unfold card.
+ intros.*)
+ (* here simplify creates problems: it seems it simplifies too much. I had to
+ * introduce the obvious theorem card_Sn.
+ *)
+ rewrite > card_Sn.
+ rewrite > (gcd_n_n (S (S n2))).
+ cut ((eqb (S (S n2)) (S O)) = false)
+ [ rewrite > Hcut.
+ simplify in \vdash (? ? ? (? % ?)).
+ rewrite > sym_plus.
+ rewrite < (plus_n_O).
+ unfold totient.
+ apply (totient_card_aux n2 n2).
+ reflexivity
+ | apply not_eq_to_eqb_false.
+ apply cic:/matita/nat/nat/not_eq_S.con.
+ unfold Not.
+ intro.
+ cut ( (S n2) \le O)
+ [ apply (not_le_Sn_n n2 ?).
+ apply (transitive_le (S n2) O n2 ? ?);
+ [ apply (Hcut)
+ | apply (le_O_n n2)
+ ]
+ | rewrite > H2.
+ apply le_n
+ ]
+ ]
+ ]
+]
+qed.
+