proposition: Lemma Zrelprime_dec : forall a b : Z, {Zrelprime a b} + {~ Zrelprime a b}.
proof: Proof. intros a b. unfold Zrelprime in |- *. case (Zdec (Zgcd a b - 1)). intro H1. left. auto with zarith. intro Hn1. right. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)