proposition: Lemma prime_rel_prime : Prime -> forall x : positive, (Zpos x < Zpos p)%Z -> Zrelprime (Zpos p) (Zpos x).
proof: Proof. intros Hprime x Hx. unfold Prime in Hprime. elim Hprime. intros H1 Hdiv. unfold Zrelprime in |- *. set (d := Zgcd (Zpos p) (Zpos x)). cut (0 < d)%Z. cut (d < Zpos p)%Z. cut (Zdivides d (Zpos p)). cut (d = Zgcd (Zpos p) (Zpos x)); auto. case d. auto with zarith. intros D HD HDiv HDlt HDpos. generalize (Hdiv D HDiv); intro H0; elim H0. intro HD1; rewrite HD1; auto. intro HDp; rewrite HDp in HDlt; elim (Zlt_irref _ HDlt). auto with zarith. unfold d in |- *; auto with zarith. apply (Z.le_lt_trans d (Zpos x) (Zpos p)); unfold d in |- *; auto with zarith. unfold d in |- *; apply Zgcd_pos; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)