proposition: Lemma coprimep_irreducible (p q : {poly R}) : ~~(p %= q) -> irreducible_poly p -> irreducible_poly q -> coprimep p q.
proof: Proof. move=> neqdpq [szpgt1 Heqdp] [szqgt1 Heqdq]. have gcdvp:= (dvdp_gcdl p q). have gcdvq:= (dvdp_gcdr p q). rewrite /coprimep; apply: contraT => neqsz1. move: (Heqdp _ neqsz1 gcdvp); rewrite eqp_sym /eqp dvdp_gcd. case/andP=> [/andP [ _ pdvq]] _. move: (Heqdq _ neqsz1 gcdvq); rewrite eqp_sym /eqp dvdp_gcd. case/andP=> [/andP [qdvp _]] _. by rewrite /eqp pdvq qdvp in neqdpq. Qed.
imports: mathcomp(all_ssreflect all_algebra)