proposition: Lemma mod_sym : forall (a b : Z) (n : nat), Mod a b n -> Mod b a n.
proof: Proof. unfold Mod 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