proposition: Lemma edivn_eq d q r : r < d -> edivn (q * d + r) d = (q, r).
proof: Proof. move=> lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd. case: edivnP lt_rd => q' r'; rewrite d_gt0 /=. wlog: q q' r r' / q <= q' by case/orP: (leq_total q q'); last symmetry; eauto. have [||-> _ /addnI ->] //= := ltngtP q q'. rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr _ eq_qr _ /lt_qr {lt_qr}. by rewrite addnS ltnNge mulSn -addnA eq_qr addnCA addnA leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)