proposition: Lemma redivp_def p q : redivp p q = (rscalp p q, rdivp p q, rmodp p q).
proof: Proof. by rewrite /rscalp /rdivp /rmodp; case: (redivp p q) => [[]] /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)