proposition: Lemma prime_decomp_correct : let pd_val pd := \prod_(f <- pd) pfactor f.1 f.2 in let lb_dvd q m := ~~ has [pred d | d %| m] (index_iota 2 q) in let pf_ok f := lb_dvd f.1 f.1 && (0 < f.2) in let pd_ord q pd := path ltn q (unzip1 pd) in let pd_ok q n pd := [/\ n = pd_val pd, all pf_ok pd & pd_ord q pd] in forall n, n > 0 -> pd_ok 1 n (prime_decomp n).
proof: Proof. rewrite unlock => pd_val lb_dvd pf_ok pd_ord pd_ok. have leq_pd_ok m p q pd: q <= p -> pd_ok p m pd -> pd_ok q m pd. rewrite /pd_ok /pd_ord; case: pd => [|[r _] pd] //= leqp [<- ->]. by case/andP=> /(leq_trans _)->. have apd_ok m e q p pd: lb_dvd p p || (e == 0) -> q < p -> pd_ok p m pd -> pd_ok q (p ^ e * m) (p ^? e :: pd). - case: e => [|e]; rewrite orbC /= => pr_p ltqp. by rewrite mul1n; apply: leq_pd_ok; apply: ltnW. by rewrite /pd_ok /pd_ord /pf_ok /= pr_p ltqp => [[<- -> ->]]. case=> // n _; rewrite /prime_decomp. case: elogn2P => e2 m2 -> {n}; case: m2 => [|[|abc]]; try exact: apd_ok. rewrite [_.-2]/= !ltnS ltn0 natTrecE; case: edivnP => a bc ->{abc}. case: edivnP => b c def_bc /= ltc2 ltbc3; apply: (apd_ok) => //. move def_m: _.*2.+1 => m; set k := {2}1; rewrite -[2]/k.*2; set e := 0. pose p := k.*2.+1; rewrite -{1}[m]mul1n -[1]/(p ^ e)%N. have{def_m bc def_bc ltc2 ltbc3}: let kb := (ifnz e k 1).*2 in [&& k > 0, p < m, lb_dvd p m, c < kb & lb_dvd p p || (e == 0)] /\ m + (b * kb + c).*2 = p ^ 2 + (a * p).*2. - rewrite -def_m [in lb_dvd _ _]def_m; split=> //=; last first. by rewrite -def_bc addSn -doubleD 2!addSn -addnA subnKC // addnC. rewrite ltc2 /lb_dvd /index_iota /= dvdn2 -def_m. by rewrite [_.+2]lock /= odd_double. have [n] := ubnP a. elim: n => // n IHn in a (k) p m b c (e) * => /ltnSE-le_a_n []. set kb := _.*2; set d := _ + c => /and5P[lt0k ltpm leppm ltc pr_p def_m]. have def_k1: k.-1.+1 = k := ltn_predK lt0k. have def_kb1: kb.-1.+1 = kb by rewrite /kb -def_k1; case e. have eq_bc_0: (b == 0) && (c == 0) = (d == 0). by rewrite addn_eq0 muln_eq0 orbC -def_kb1. have lt1p: 1 < p by rewrite ltnS double_gt0. have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double. have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)]. move=> d0; have{d0} def_m: m = (p + a.*2) * p. by rewrite d0 addn0 -!mul2n mulnA -mulnDl in def_m *. split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r. by rewrite def_m dvdn_mull. by rewrite def_m dvdn_mulr. case def_a: a => [|a'] /= in le_a_n *; rewrite !natTrecE -/p {}eq_bc_0. case: d if_d0 def_m => [[//| def_m {}pr_p pr_m'] _ | d _ def_m] /=. rewrite def_m def_a addn0 mulnA -2!expnSr. by split; rewrite /pd_ord /pf_ok /= ?muln1 ?pr_p ?leqnn. apply: apd_ok; rewrite // /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm. rewrite /pf_ok !andbT /=; split=> //; apply: contra leppm. case/hasP=> r /=; rewrite mem_index_iota => /andP[lt1r ltrm] dvrm; apply/hasP. have [ltrp | lepr] := ltnP r p. by exists r; rewrite // mem_index_iota lt1r. case/dvdnP: dvrm => q def_q; exists q; last by rewrite def_q /= dvdn_mulr. rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1r)) -def_q mul1n ltrm. move: def_m; rewrite def_a addn0 -(@ltn_pmul2r p) // mulnn => <-. apply: (@leq_ltn_trans m); first by rewrite def_q leq_mul. by rewrite -addn1 leq_add2l. have def_k2: k.*2 = ifnz e 1 k * kb. by rewrite /kb; case: (e) => [|e']; rewrite (mul1n, muln2). case def_b': (b - _) => [|b']; last first. have ->: ifnz e k.*2.-1 1 = kb.-1 by rewrite /kb; case e. apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split=> //. rewrite lt0k ltpm leppm pr_p andbT /=. by case: ifnzP; [move/ltn_predK->; apply: ltnW | rewrite def_kb1]. apply: (@addIn p.*2). rewrite -2!addnA -!doubleD -addnA -mulSnr -def_a -def_m /d. have ->: b * kb = b' * kb + (k.*2 - c * kb + kb). rewrite addnCA addnC -mulSnr -def_b' def_k2 -mulnBl -mulnDl subnK //. by rewrite ltnW // -subn_gt0 def_b'. rewrite -addnA; congr (_ + (_ + _).*2). case: (c) ltc; first by rewrite -addSnnS def_kb1 subn0 addn0 addnC. rewrite /kb; case e => [[] // _ | e' c' _] /=; last first. by rewrite subnDA subnn addnC addSnnS. by rewrite mul1n -doubleB -doubleD subn1 !addn1 def_k1. have ltdp: d < p. move/eqP: def_b'; rewrite subn_eq0 -(@leq_pmul2r kb); last first. by rewrite -def_kb1. rewrite mulnBl -def_k2 ltnS -(leq_add2r c); move/leq_trans; apply. have{} ltc: c < k.*2. by apply: (leq_trans ltc); rewrite leq_double /kb; case e. rewrite -{2}(subnK (ltnW ltc)) leq_add2r leq_sub2l //. by rewrite -def_kb1 mulnS leq_addr. case def_d: d if_d0 => [|d'] => [[//|{ltdp pr_p}def_m pr_p pr_m'] | _]. rewrite eqxx -doubleS -addnS -def_a doubleD -addSn -/p def_m. rewrite mulnCA mulnC -expnSr. apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split. rewrite lt0k -addn1 leq_add2l {1}def_a pr_m' pr_p /= def_k1 -addnn. by rewrite leq_addr. rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr. by rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn. have next_pm: lb_dvd p.+2 m. rewrite /lb_dvd /index_iota (addKn 2) -(subnK lt1p) iotaD has_cat. apply/norP; split; rewrite //= orbF subnKC // orbC. apply/norP; split; apply/dvdnP=> [[q def_q]]. case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k). by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double. move/(congr1 (dvdn p)): def_m; rewrite -!mul2n mulnA -mulnDl. rewrite dvdn_mull // dvdn_addr; last by rewrite def_q dvdn_mull. case/dvdnP=> r; rewrite mul2n => def_r; move: ltdp (congr1 odd def_r). rewrite odd_double -ltn_double def_r -mul2n ltn_pmul2r //. by case: r def_r => [|[|[]]] //; rewrite def_d // mul1n /= odd_double. apply: apd_ok => //; case: a' def_a le_a_n => [|a'] def_a => [_ | lta] /=. rewrite /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm /pf_ok !andbT /=. split=> //; apply: contra next_pm. case/hasP=> q; rewrite mem_index_iota => /andP[lt1q ltqm] dvqm; apply/hasP. have [ltqp | lepq] := ltnP q p.+2. by exists q; rewrite // mem_index_iota lt1q. case/dvdnP: dvqm => r def_r; exists r; last by rewrite def_r /= dvdn_mulr. rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1q)) -def_r mul1n ltqm /=. rewrite -(@ltn_pmul2l p.+2) //; apply: (@leq_ltn_trans m). by rewrite def_r mulnC leq_mul. rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnACA. by rewrite def_a mul1n in def_m; rewrite -def_m addnS /= ltnS -addnA leq_addr. set bc := ifnz _ _ _; apply: leq_pd_ok (leqnSn _) _. rewrite -doubleS -{1}[m]mul1n -[1]/(k.+1.*2.+1 ^ 0)%N. apply: IHn; first exact: ltnW. rewrite doubleS -/p [ifnz 0 _ _]/=; do 2?split => //. rewrite orbT next_pm /= -(leq_add2r d.*2) def_m 2!addSnnS -doubleS leq_add. - move: ltc; rewrite /kb {}/bc andbT; case e => //= e' _; case: ifnzP => //. by case: edivn2P. - by rewrite -[ltnLHS]muln1 ltn_pmul2l. by rewrite leq_double def_a mulSn (leq_trans ltdp) ?leq_addr. rewrite mulnDl !muln2 -addnA addnCA doubleD addnCA. rewrite (_ : _ + bc.2 = d); last first. rewrite /d {}/bc /kb -muln2. case: (e) (b) def_b' => //= _ []; first by case: edivn2P. by case c; do 2?case; rewrite // mul1n /= muln2. rewrite def_m 3!doubleS addnC -(addn2 p) sqrnD mul2n muln2 -3!addnA. congr (_ + _); rewrite 4!addnS -!doubleD; congr _.*2.+2.+2. by rewrite def_a -add2n mulnDl -addnA -muln2 -mulnDr mul2n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)