proposition: Lemma edivnP : forall m d, edivn_spec m d (edivn m d).
proof: Proof. rewrite /edivn => m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m). elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn. rewrite subn_if_gt; case: ltnP => [// | le_dm]. rewrite -{1}(subnK le_dm) [_ + d]addnC -addSn addnA -mulSnr; apply: IHn. apply: leq_trans le_mn; exact: leq_subr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div)