proposition: Theorem rel_prime_le_prime: forall a p, prime p -> 1 <= a < p -> rel_prime a p.
proof: Proof. intros a p Hp [H1 H2]. apply rel_prime_sym; apply prime_rel_prime; auto. intros [q Hq]; subst a. destruct Hp as [H3 H4]. contradict H2; apply Zle_not_lt. rewrite <- (Z.mul_1_l p) at 1. apply Zmult_le_compat_r. - apply (Zlt_le_succ 0). apply Zmult_lt_0_reg_r with p. + apply Z.le_succ_l, Z.lt_le_incl; auto. + now apply Z.le_succ_l. - apply Z.lt_le_incl, Z.le_succ_l, Z.lt_le_incl; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat