proposition: Lemma dvdp_eqp1 p q : p %| q -> q %= 1 -> p %= 1.
proof: Proof. move=> dpq hq. have sizeq : size q == 1 by rewrite size_poly_eq1. have n0q : q != 0 by case: eqP hq => // ->; rewrite eqp01. rewrite -size_poly_eq1 eqn_leq -{1}(eqP sizeq) dvdp_leq //= size_poly_gt0. by apply/eqP => p0; move: dpq n0q; rewrite p0 dvd0p => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)