proposition: Lemma zmod_minus_compat : forall a b c d n : Z, ZMod a b n -> ZMod c d n -> ZMod (a - c) (b - d) n.
proof: Proof. intros. unfold Zminus in |- *. apply zmod_plus_compat. assumption. apply zmod_opp_compat. assumption. Qed.
imports: ZArith lemmas natZ exp divides