proposition: Lemma zmod_sym : forall a b n : Z, ZMod a b n -> ZMod b a n.
proof: Proof. unfold ZMod in |- *. intros. elim H. intros. split with (- x)%Z. simpl in |- *. rewrite H0. simpl in |- *. rewrite Zplus_assoc_reverse. rewrite <- Zmult_plus_distr_r. rewrite Zplus_opp_r. rewrite <- Zmult_0_r_reverse. apply Zplus_0_r_reverse. Qed.
imports: ZArith lemmas natZ exp divides