proposition: Lemma Zrelprime_nonzero_lft : forall a b : Z, Zrelprime a b -> Z.abs b <> 1%Z -> a <> 0%Z.
proof: Proof. intros. apply (Zrelprime_nonzero_rht b a). apply Zrelprime_symm. assumption. assumption. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)