proposition: Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
proof: Proof. intros n H H1; absurd (n = 1 \/ n = -1). - intros [H2 | H2]; subst; contradict H; discriminate. - case (Zis_gcd_unique 0 n n 1); auto. apply Zis_gcd_intro; auto. + exists 0; reflexivity. + exists 1; rewrite Z.mul_1_l; reflexivity. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat