proposition: Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
proof: Proof. intros a b H H1 H2. case (not_rel_prime_0 _ H). rewrite <- H2. apply rel_prime_mod; auto. now transitivity 1. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat