proposition: Lemma zmod_opp_compat : forall a b n : Z, ZMod a b n -> ZMod (- a) (- b) n.
proof: Proof. intros. elim H. intros. split with (- x)%Z. rewrite H0. rewrite Zopp_eq_mult_neg_1. rewrite Zopp_eq_mult_neg_1. rewrite Zopp_eq_mult_neg_1. rewrite Zmult_assoc. rewrite <- Zmult_plus_distr_l. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides