proposition: Lemma Zm_non_triv : (ZModap 1 0).
proof: Proof. unfold ZModap. intro Hfalse. generalize (Zmodeq_modeq _ _ _ Hfalse). rewrite Zmod_zero_lft. rewrite Zmod_one_lft; auto. intro H. assert False. discriminate. elim H0. exact m_gt_1. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields