proposition: Lemma Zdivides_minus_elim : forall a b c : Z, Zdivides a b -> Zdivides a c -> Zdivides a (b - c).
proof: Proof. intros. unfold Zminus in |- *. apply Zdivides_plus_elim. assumption. apply Zdivides_opp_elim_rht. assumption. Qed.
imports: CoRN.model.Zmod.ZBasics