proposition: Lemma divE x y : Nat.div x y = divn x y.
proof: Proof. case: y => [//|y]. rewrite /Nat.div. move: (Nat.divmod_spec x y 0 y). case: Nat.divmod => q r /(_ (le_n _)) []. rewrite Nat.mul_0_r Nat.sub_diag !Nat.add_0_r Nat.mul_comm => + Hr /=. rewrite multE minusE plusE => /(f_equal (fun x => divn x y.+1)) ->. rewrite divnMDl // divn_small ?addn0 //. rewrite ltn_subLR; [|exact/ssrnat.leP]. by rewrite -addSnnS addnC addnS ltnS leq_addr. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)