proposition: Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a) mod b = b - (a mod b).
proof: Proof. intros a b. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms