proposition: Lemma sdvdr_wf : well_founded (@sdvdr [dvdRingType of R]).
proof: Proof. move=> a; wlog: a / a != 0=> [ha|]. case a0: (a == 0); last by apply: ha; rewrite a0. rewrite (eqP a0); constructor=> b; rewrite sdvdr0; apply: ha. elim: (norm a) {-2}a (leqnn (norm a))=> [|n ihn] {}a ha a0. by constructor=> x; move/(ltn_norm a0); rewrite ltnNge (leq_trans ha) ?leq0n. constructor=> x hx; move/(ltn_norm a0):(hx)=> hn; apply ihn. by rewrite -ltnS (leq_trans hn). by apply: contra a0; move/eqP=> x0; move/sdvdrW:hx; rewrite x0 dvd0r. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete