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