- ]
- | rewrite < (sigma_p2' n n
- (\lambda d:nat.divides_b d (pred n))
- (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
- (\lambda x,y.(S O))).
- apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
- [ apply (eq_sigma_p_gh
- (\lambda x:nat. (S O))
- (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
- (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
- (n*n)
- (pred n)
- (\lambda x:nat.
- divides_b (x/n) (pred n)
- \land (leb (S (x \mod n)) (x/n)
- \land eqb (gcd (x \mod n) (x/n)) (S O)))
- (\lambda x:nat.true)
- )
- [ intros.
- reflexivity
- | intros.
- cut ((i/n) \divides (pred n))
- [ cut ((i \mod n ) \lt (i/n))
- [ cut ((gcd (i \mod n) (i / n)) = (S O))
- [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
- [ rewrite > Hcut3.
- cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
- [ rewrite > Hcut4.
- cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
- [ rewrite > Hcut5.
- apply sym_eq.
- apply div_mod.
- apply (trans_lt O (S O) n)
- [ apply (lt_O_S O)
- | assumption
- ]
- | elim Hcut.
- rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
- rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
- rewrite > (div_times_ltO n2 (i/n))
- [ rewrite > H3.
- apply div_times_ltO.
- apply (divides_to_lt_O n2 (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness n2 (pred n) (i/n)).
- rewrite > sym_times.
- assumption
- ]
- | apply (divides_to_lt_O (i/n) (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness (i/n) (pred n) n2).
- assumption
- ]
- ]
- ]
- | elim Hcut.
- cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
- [ rewrite > Hcut4.
- rewrite > H3.
- rewrite < (sym_times n2 (i/n)).
- rewrite > (div_times_ltO n2 (i/n))
- [ rewrite > (div_times_ltO (i \mod n) n2)
- [ reflexivity
- | apply (divides_to_lt_O n2 (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness n2 (pred n) (i/n)).
- rewrite > sym_times.
- assumption
- ]
- ]
- | apply (divides_to_lt_O (i/n) (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).