proposition: Lemma mod_minus_compat : forall (a b c d : Z) (n : nat), Mod a b n -> Mod c d n -> Mod (a - c) (b - d) n.
proof: Proof. intros. unfold Zminus in |- *. apply mod_plus_compat. assumption. apply mod_opp_compat. assumption. Qed.
imports: ZArith lemmas natZ exp divides