proposition: Lemma krull1_adequate a b : { r : R & adequate_spec a b r }.
proof: Proof. have [] := eqVneq b 0; first by exists 0; constructor. move: (krull1_factor a b) => factored. have /sigW : (exists (x : nat * (R * R)), [&& 0 < x.1, b == x.2.1 * x.2.2, coprimer x.2.1 a & x.2.2 %| a ^+ x.1]). by case: factored => n [b1 [b2]]; exists (n,(b1,b2)). case=> /= [[n [b1 b2]]] /= /and4P [ngt0 /eqP -> ca1b dvda2bn aneq0]. exists b1; constructor => /= [|||d] //; first by rewrite dvdr_mulr. rewrite mulrC dvdr_mul2l ?unitd1 => [dvdda2|]. apply: contra; rewrite -(@coprimer_pexpr _ n) //. apply: dvdr_coprime; exact: (dvdr_trans dvdda2 dvda2bn). by apply: contraNneq aneq0 => ->; rewrite mul0r. 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