proposition: Lemma rdvdp_trans (p q r : {poly R}) : p \is monic -> q \is monic -> rdvdp p q -> rdvdp q r -> rdvdp p r.
proof: Proof. move=> pM qM /rdvdpP => /(_ pM) [qq1 qq1E] /rdvdpP => /(_ qM) [qq2 qq2E]. by apply/rdvdpP => //; exists (qq2 * qq1); rewrite qq2E qq1E mulrA. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)