proposition: Lemma irredr_primer : forall a, irredr a <-> primer a.
proof: Proof. move=> a; split=> ia; rewrite /primer /irredr !ia; do ![split]=> b c. apply/idP/idP; last by case/orP=> ha; [rewrite dvdr_mulr|rewrite dvdr_mull]. rewrite [_ %| b]irredr_dvd //; case cab: (coprimer _ _)=> //=. by rewrite mulrC euclid. have [-> | b0] := eqVneq b 0; first by rewrite mul0r eqdr0 ia. have [-> | c0] := eqVneq c 0; first by rewrite mulr0 eqdr0 ia. rewrite eqd_def ia andb_orl. case/orP; case/andP; move/(dvdr_trans _)=> h; move/h. by rewrite dvdr_mull_l // => ->; rewrite orbT. by rewrite dvdr_mulr_l // => ->. 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