proposition: Lemma irredrP : forall a, irredr a -> forall b c, a %= b * c -> b %= 1 \/ c %= 1.
proof: Proof. by move=> ? [ha ia] *; apply/orP; rewrite ia. 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