proposition: Lemma Zp_nonz_mod: 0<(Z.modulo x m)<m.
proof: Proof. generalize (Z_mod_lt x m); intro H; elim H; clear H; intros. split. elim (Zlt_asymmetric (Z.modulo x m) 0). intro Hfalse; elim Hx; elim Hfalse; clear Hfalse; intro Hfalse. elim H; apply Z.lt_gt; auto. simpl; rewrite <-Hfalse; auto with zarith. apply Z.gt_lt. assumption. exact p_gt_0. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields