proposition: Lemma Zrelprime_nonzero_rht : forall a b : Z, Zrelprime a b -> Z.abs a <> 1%Z -> b <> 0%Z.
proof: Proof. intros a b H Ha. intro Hfalse. rewrite Hfalse in H. unfold Zrelprime in H. rewrite Zgcd_zero_rht in H. tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)