proposition: Lemma divp_eq p : p = (p %/ d) * d + (p %% d).
proof: Proof. by have := divp_eq p d; rewrite scalpE ulcd expr0 scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)