proposition: Fact Op_divn_subproof n m : Z.of_nat (n %/ m) = divZ (Z.of_nat n) (Z.of_nat m).
proof: Proof. by case: n m => [|n] [|m]; rewrite /divZ //= ?SuccNat2Pos.id_succ; case: divn. Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)