proposition: Lemma irredr_dvd : forall a b, irredr a -> a %| b = ~~(coprimer a b) :> bool.
proof: Proof. rewrite /coprimer=> a b ia; case g1: (_ %= 1)=> /=. apply/negP=> hab; suff: a %= 1 by rewrite ia. by rewrite -dvdr1 (@dvdr_trans _ (gcdr a b)) ?dvdr_gcd ?dvdrr // dvdr1. case: (dvdrP _ _ (dvdr_gcdl a b))=> x hx; rewrite hx. move/eq_eqd: hx; case/irredrP => //; last by rewrite g1. move=> hx; rewrite (eqd_dvd (eqd_mul hx (eqdd _)) (eqdd _)). by rewrite mul1r dvdr_gcdr. 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