-
-(*the following theorem is just a particular case of the theorem
- divides_times, prooved in primes.ma
- *)
-theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
-a \divides b \to a \divides (b*c).
-intros.
-rewrite > (times_n_SO a).
-apply (divides_times).
-assumption.
-apply divides_SO_n.
-qed.
-
-theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
-i < n*n \to
- (divides_b (i/n) (pred n)
-\land (leb (S(i\mod n)) (i/n)
-\land eqb (gcd (i\mod n) (i/n)) (S O)))
- =true
- \to i\mod n*pred n/(i/n)<(pred n).
-intros.
-apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
- ((i/n)*(pred n) / (i/n))
- (pred n))
-[ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n)))
- [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption.
- | rewrite > (NdivM_times_M_to_N )
- [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
- [ apply (monotonic_lt_times_variant (pred n))
- [ apply (nat_case1 n)
- [ intros.
- rewrite > H2 in H:(? ? %).
- change in H:(? ? %) with (O).
- change in H:(%) with ((S i) \le O).
- apply False_ind.
- apply (not_le_Sn_O i H)
- | intro.
- elim m
- [ rewrite > H2 in H1:(%).
- rewrite > H2 in H:(%).
- simplify in H.
- cut (i = O)
- [ rewrite > Hcut in H1:(%).
- simplify in H1.
- apply False_ind.
- apply (not_eq_true_false H1)
- | change in H:(%) with((S i) \le (S O)).
- cut (i \le O )
- [ apply (nat_case1 i)
- [ intros.
- reflexivity
- | intros.
- rewrite > H3 in Hcut:(%).
- apply False_ind.
- apply (not_le_Sn_O m1 Hcut)
- ]
- | apply (le_S_S_to_le i O).
- assumption
- ]
- ]
- | change with ((S O) \le (S n1)).
- apply (le_S_S O n1).
- apply (le_O_n n1)
- ]
- ]
- | change with ((S (i\mod n)) \le (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption
- ]
- | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
+(*tha main theorem*)
+theorem sigma_p_Sn_divides_b_totient_n: \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
+intros.
+unfold totient.
+apply (trans_eq ? ?
+(sigma_p (S n) (\lambda d:nat.divides_b d n)
+(\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
+[ apply eq_sigma_p1
+ [ intros.
+ reflexivity
+ | intros.
+ apply sym_eq.
+ apply (trans_eq ? ?
+ (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
+ [ apply false_to_eq_sigma_p
+ [ apply lt_to_le.
+ assumption
+ | intros.
+ rewrite > lt_to_leb_false
+ [ reflexivity
+ | apply le_S_S.