proposition: Lemma mod_opp_compat : forall (a b : Z) (n : nat), Mod a b n -> Mod (- 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