proposition: Lemma divp1 m : m %/ 1 = m.
proof: Proof. by rewrite divpE lead_coefC unitr1 Ring.rdivp1 expr1n invr1 scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)