proposition: Lemma expp_sub m n : n <= m -> (d ^+ (m - n))%N = d ^+ m %/ d ^+ n.
proof: Proof. by move/subnK=> {2}<-; rewrite exprD mulpK // lead_coef_exp unitrX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)