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