proposition: Lemma pp_prim_eq : forall p, p != 0 -> primitive p = (p %= pp p).
proof: Proof. move=> p p0. apply/idP/idP; first exact: pp_prim. case/andP=> H _. move: (prim_pp p0). rewrite /primitive eqd_def; case/andP=> gp1 _. move: H; rewrite dvdrp_spec; case/andP=> gp2 _. by apply/andP; rewrite (dvdr_trans gp2 gp1) dvd1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)