proposition: Lemma edivn_eq_left : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
proof: Proof. move=> d q r lt_rd; have d_pos: 0 < d by exact: leq_trans lt_rd. case: (edivnP_left (q * d + r) d) lt_rd; rewrite d_pos /=. set q':= (edivn (q * d + r) d).1; set r':= (edivn (q * d + r) d).2. rewrite (surjective_pairing (edivn (q * d + r) d)) -/q' -/r'. wlog: q r q' 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)