proposition: Fact Op_divz_subproof n m : Z_of_int (divz n m) = divZ (Z_of_int n) (Z_of_int m).
proof: Proof. case: n => [[|n]|n]; rewrite /divz /divZ /= ?addn1 /=; nia. Qed.
imports: Coq(ZArith ZifyClasses ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial ssralg countalg ssrnum ssrint rat) mathcomp(intdiv) mathcomp(zify_ssreflect ssrZ)