proposition: Lemma Zm_opp_strext : (un_op_strext _ Zm_opp).
proof: Proof. red; red; simpl. intros x y. unfold ZModeq; unfold ZModap; unfold Zm_plus; unfold Zm_opp. intro Hneq. intro Heq. apply Hneq. apply Zmodeq_opp_elim. exact Heq. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields