proposition: Lemma Zp_is_CField: (is_CField Zp Zp_inv).
proof: Proof. red; red. intros x. simpl; unfold ZModap; unfold ZModeq; unfold Zm_mult; unfold Zp_inv. intros Hx. elim (Zp_nonz_mod x Hx); intros Hxmod0 Hxmodp. split. apply Zmodeq_eqmod. rewrite Zmod_one_lft; auto. apply Zmod_relprime_inv; auto. exact p_gt_1. apply Zrelprime_symm. unfold Zrelprime. rewrite <-Zgcd_mod_rht; auto. generalize Hxmod0. set (d:=(Z.modulo x m)). cut (d=(Z.modulo x m)); auto. case d. intros _ Hfalse; elim (Zlt_irref _ Hfalse). intros D HD _. rewrite <-HD in Hxmodp. elim (prime_rel_prime m Hprime D Hxmodp); auto. intros D _ Hfalse; elim (Zge_0_NEG _ Hfalse). exact p_gt_0. exact p_gt_1. apply Zmodeq_eqmod. rewrite Zmod_one_lft; auto. cut ((x * Zgcd_coeff_a x m) mod m = 1). intro H; elim H. apply Zmodeq_wd. apply Zmult_comm. apply Zmod_relprime_inv; auto. exact p_gt_1. apply Zrelprime_symm. unfold Zrelprime. rewrite <-Zgcd_mod_rht; auto. generalize Hxmod0. set (d:=(Z.modulo x m)). cut (d=(Z.modulo x m)); auto. case d. intros _ Hfalse; elim (Zlt_irref _ Hfalse). intros D HD _. rewrite <-HD in Hxmodp. elim (prime_rel_prime m Hprime D Hxmodp); auto. intros D _ Hfalse; elim (Zge_0_NEG _ Hfalse). exact p_gt_0. exact p_gt_1. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields