proposition: Lemma krull1_factor a b : exists n b1 b2, [&& 0 < n, b == b1 * b2, coprimer b1 a & b2 %| a ^+ n].
proof: Proof. wlog suff: / exists n b1 b2, [&& 0 < n, b %= b1 * b2, coprimer b1 a & b2 %| a ^+ n]. case=> n [b1 [b2 /and4P [Hn Hb Hb1 Hb2]]]. have [b2_eq0|b2_neq0] := eqVneq b2 0. exists n, b1, b2; move: Hn Hb Hb1 Hb2. by rewrite b2_eq0 mulr0 eqdr0 => -> -> -> ->. have : b2 %| b by rewrite (eqd_dvdr _ Hb) dvdr_mull. case: dvdrP Hb => [[b1' ->]|//]; rewrite eqd_mul2r // => eq_b1'. exists n, b1', b2; rewrite !eqxx Hn Hb2 /coprimer andbT /=. by rewrite (eqd_ltrans (eqd_gcd eq_b1' (eqdd _))). have kidem x : exists d (s : R) k, [&& 0 < d, b %| s ^+ 2 - s, b %| x ^+ d - (x ^+ d) * s & b %| s - k * x ^+ d]. have [m [y]] := krull1 b x. have [-> Hy|m_gt0 Hy] := posnP m. exists 1%N, 1, y; rewrite !expr1n mulr1 expr1 !subrr dvdr0 /=. by move: Hy; rewrite expr0 mul1r mulrC. set s := (x * y) ^+ m; exists m, s, (y ^+ m). have xsn n : b %| x ^+ m * (x * y) ^+ n - x ^+ m. elim: n => [|n ihn]; first by rewrite mulr1 subrr dvdr0. rewrite -[X in X - _](addrNK (x ^+ m * (x * y) ^+ n)) -addrA dvdr_add //. rewrite exprS mulrA -mulrBl dvdr_mulr //. by rewrite -dvdrN opprB -[X in X - _]mulr1 -mulrBr. have s_idem n : b %| s * (x * y) ^+ n - s. elim: n => [|n ihn]; first by rewrite mulr1 subrr dvdr0. rewrite -[X in X - _](addrNK (s * (x * y) ^+ n)) -addrA dvdr_add //. rewrite exprS mulrA -mulrBl dvdr_mulr //. rewrite /s -exprSr !exprMn exprSr exprS mulrA -mulrBl dvdr_mulr //. by rewrite -dvdrN opprB -{1}[x ^+ m]mulr1 -mulrA -mulrBr. rewrite m_gt0 (s_idem m) /= -opprB dvdrN (xsn m) /=. by rewrite mulrC -exprMn subrr dvdr0. have [d [s [k /and4P [d_gt0 s_idem ads ska]]]] := kidem a. set b1 := gcdr b (1 - s); set b2 := gcdr b s; exists d, b1, b2. have dvd_b2_bd: b2 %| a ^+ d. rewrite -[a ^+ d](addrNK (a ^+ d * s)) dvdr_add ?andbT //=; last 2 first. by rewrite (dvdr_trans (dvdr_gcdl _ _)) //. by rewrite dvdr_mull // dvdr_gcdr. have eq_b : b %= b1 * b2. rewrite eqd_def /b1 /b2. rewrite -[b as X in _ %| X](addrNK (b * s)). rewrite -[X in X - b * s]mulr1 -mulrBr dvdr_add ?andbT //=; last 2 first. by rewrite mulrC dvdr_mul // (dvdr_gcdl, dvdr_gcdr). by rewrite dvdr_mul // (dvdr_gcdl, dvdr_gcdr). have [[x y gbs] [x' y' gbs']] := (bezoutP b s, bezoutP b (1 - s)). rewrite (eqd_dvdr _ (eqd_mulr _ gbs')) (eqd_dvdr _ (eqd_mull _ gbs)). rewrite [1 - s]lock !(mulrDr, mulrDl) -!lock !addrA dvdr_add //=. by rewrite ![_ * b * _](mulrAC, mulrA) !mulrA -!mulrDl dvdr_mull. by rewrite mulrCA -mulrA dvdr_mull // dvdr_mull // mulrBl mul1r -opprB dvdrN. rewrite dvd_b2_bd eq_b d_gt0 andbT //=. have: coprimer b1 b2. apply: gcdr_def; rewrite ?dvd1r //= => p ps' ps. rewrite -[1](addrNK s) dvdr_add //. by rewrite (dvdr_trans ps') ?dvdr_gcdr. by rewrite (dvdr_trans ps) ?dvdr_gcdr. have b2_eq : gcdr b s %= gcdr b (a ^+ d). rewrite eqd_def !dvdr_gcd !dvdr_gcdl /=. rewrite -[a ^+ d as X in _ %| X](addrNK ((a ^+ d) * s)). rewrite dvdr_add //=; last 2 first. by rewrite (dvdr_trans (dvdr_gcdl _ _)). by rewrite dvdr_mull ?dvdr_gcdr. rewrite -[s as X in _ %| X](addrNK (k * (a ^+ d))) dvdr_add //. by rewrite (dvdr_trans (dvdr_gcdl _ _)). by rewrite dvdr_mull ?dvdr_gcdr. rewrite /b2 /coprimer (eqd_ltrans (eqd_gcd (eqdd _) b2_eq)). rewrite (eqd_ltrans (gcdrA _ _ _)). have gb1b: gcdr b1 b %= b1. rewrite eqd_def dvdr_gcdl dvdr_gcd dvdrr /=. by rewrite (eqd_dvdr _ eq_b) dvdr_mulr. rewrite (eqd_ltrans (eqd_gcd gb1b (eqdd _))). apply: coprimer_dvdr. by rewrite -[d]prednK // exprS dvdr_mulr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr