proposition: Lemma Zp_nonz_relprime: (Zrelprime x m).
proof: Proof. simpl in Hx. unfold ZModap in Hx; unfold ZModeq in Hx. elim Zp_nonz_mod; intros Hxmod0 Hxmodp. unfold Zrelprime. rewrite <-Zgcd_mod_lft; auto. generalize Hxmod0. set (d:=(Z.modulo x m)). cut (d=(Z.modulo x m)). case d. intros _ Hfalse; elim (Zlt_irref _ Hfalse). intros D HD _. rewrite <-HD in Hxmodp. rewrite Zgcd_symm. elim (prime_rel_prime m Hprime D Hxmodp); auto. intros D _ Hfalse; elim (Zge_0_NEG _ Hfalse). auto. exact p_gt_0. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields