proposition: Fact divZ_eq m d : m = (divZ m d * d + modZ m d)%Z.
proof: Proof. rewrite /modZ; lia. 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)