-(* da spostare *)
-lemma gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
-intro.apply (nat_case n)
- [intros.reflexivity
- |intros.
- apply le_to_le_to_eq
- [apply divides_to_le
- [apply lt_O_S|apply divides_gcd_n]
- |apply divides_to_le
- [apply lt_O_gcd.rewrite > (times_n_O O).
- apply lt_times[apply lt_O_S|assumption]
- |apply divides_d_gcd
- [apply (witness ? ? m1).reflexivity
- |apply divides_n_n
+(*this obvious property is useful because simplify, sometimes,
+ "simplifies too much", and doesn't allow to obtain this simple result.
+ *)
+theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
+card (S n) p = (bool_to_nat (p (S n))) + (card n p).
+intros.
+simplify.
+reflexivity.
+qed.
+
+(* 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