proposition: Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d).
proof: Proof. Admitted. Lemma edivnP_left : forall m d, edivn_spec_left m d (edivn m d). Admitted. Lemma edivn_eq_right : forall d q r, r < d -> edivn (q * d + r) d = (q, r). Proof. move=> d q r lt_rd; have d_pos: 0 < d by exact: leq_trans lt_rd. set m := q * d + r; have: m = q * d + r by []. set d' := d; have: d' = d by []. case: (edivnP_right m d') => {d'}m d' q' r' -> lt_r'd' d'd q'd'r'. move: q'd'r' lt_r'd' lt_rd; rewrite d'd d_pos {d'd m} /=. wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto. rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->. rewrite -(leq_pmul2r d_pos); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}. by rewrite addnS ltnNge mulSn -addnA -Eqr addnCA addnA leq_addr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div)