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