proposition: Fact modZ_ge0 m d : d <> 0%Z -> (0 <= modZ m d)%Z.
proof: Proof. by move: d m => [] // d [] // m _; rewrite /modZ /divZ [Z.abs_nat _]/=; move: (leq_trunc_div (Pos.to_nat m) (Pos.to_nat d)); move: (@ltn_ceil (Pos.to_nat m).-1 (Pos.to_nat d)); 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)