proposition: Lemma edivnP m d : edivn_spec m d (edivn m d).
proof: Proof. rewrite -[m in edivn_spec m]/(0 * d + m) /edivn; case: d => //= d. elim/ltn_ind: m 0 => -[|m] IHm q //=; rewrite subn_if_gt. case: ltnP => // le_dm; rewrite -[in m.+1](subnKC le_dm) -addSn. by rewrite addnA -mulSnr; apply/IHm/leq_subr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)