proposition: Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> a mod (-b) = (a mod b) - b.
proof: Proof. intros a b ?. now zero_or_not b; [destruct a|apply Z.mod_opp_r_nz]. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms