proposition: Lemma coprime_example p q: coprime p q -> (p -c \1c) *c (q -c \1c) = cdouble(csumb q (fun k => (k *c p) %/c q)).
proof: Proof. move => cpq. have H s: natp s -> \0c %/c s = \0c by move/cdivision_of_zero; case. case: (equal_or_not q \0c) => qz. by rewrite qz (cdiff_wrong cle_01) cprod0r csum_trivial0 cdouble0. case: (equal_or_not q \1c) => qo. rewrite qo cdiff_nn cprod0r csum_trivial3 cprod0l. by rewrite(H _ NS1) cardinal_set0 cdouble0. move:(cpq) => [pN qN _]. move:(cge2 (CS_nat qN) qz qo) => qge2. move:(cdiff_pr qge2) (NS_diff \2c qN); set q2 := _ -c _ => q2v q2N. have q1N := NS_succ q2N. have q2v': q = csucc (csucc q2). by rewrite (Nsucc_rw q1N) (Nsucc_rw q2N)- csumA csum_11 csumC - q2v. pose f i := ((csucc i) *c p) %/c q. set X := csumb _ _. have ->: X = csumb (csucc q2) f. rewrite /X {1}q2v' (fct_sum_rec1 _ q1N) cprod0l(H _ qN) csum0r //. apply:CS_cardinal. rewrite cdoubleE {1} (fct_sum_rev f q2N) sum_of_sums. rewrite q2v' -(cpred_pr4 (CS_succ _)) (cpred_pr2 q1N) - csum_of_same. apply:csumb_exten => i /(NltP q1N) /(cltSleP q2N) lin /=; rewrite /f. have iN:=(NS_le_nat lin q2N). have ha: natp (csucc (q2 -c i) *c p) by fprops. have hb: natp (csucc i *c p) by fprops. move: (cdivision ha qN qz) (cdivision hb qN qz). set A := _ %/c _; set B := _ %/c _; set r1 := _ %%c _; set r2 := _ %%c _. move => [AN r1N [div1 lt1]] [BN r2N [div2 lt2]]. have: q *c p = csucc (q2 -c i) *c p +c csucc i *c p. rewrite - cprodDl (csum_Sn _ (NS_diff i q2N)) (csum_nS _ iN) csumC. by rewrite (cdiff_pr lin) q2v'. have ABN:= NS_sum AN BN. rewrite div1 div2 csumACA - cprodDr => hc. move:(cdivides_pr1 pN qN) (cdivides_pr1 ABN qN);rewrite hc => d1 d2. move: (cdivides_pr (cdivides_diff1 (NS_sum r1N r2N) d2 d1)) => eq3. move:(csum_Mlelt qN (proj1 lt1) lt2); rewrite eq3 csum_nn cprodC. move/(cprod_lt2r qN (NS_quo q (NS_sum r1N r2N)) NS2) => /clt2; case => eq4. move: eq3; rewrite eq4 cprod0r => /csum_nz [_ r2z]. move:(cdivides_pr1 BN qN);rewrite -(csum0r (CS_prod2 q B)) - r2z -div2 => dd. move:(cdivides_pr (coprime3 (coprime_S cpq) (NS_succ iN) dd)). move:(NS_quo q (NS_succ iN)); set C := _ %/c _ => cN eq2. case: (equal_or_not C \0c) => cz. by move:(@succ_nz i); rewrite eq2 cz cprod0r. move:(cltS q1N). move:(cprod_Meqle q (cge1 (CS_nat cN) cz)). rewrite (cprod1r (CS_nat qN)) - eq2 q2v' => ra. case: (cltNge (clt_leT (cltS q1N) ra)). by move /(cleSSP (CS_nat iN) (CS_nat q2N)): lin. move: hc; rewrite eq3 eq4 - cprodDr. move/(cprod_eq2l qN pN (NS_sum ABN NS1) qz) => ->; exact:(cdiff_pr1 ABN NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)