proposition: Lemma Zrelprime_irref : forall a : Z, (a > 1)%Z -> ~ Zrelprime a a.
proof: Proof. intros a Ha. unfold Zrelprime in |- *. rewrite Zgcd_idemp. auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)