proposition: Lemma edivn_eq : 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 lt_rd => q' r'; rewrite d_pos /=. 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)