proposition: Lemma Zm_plus_strext : (bin_fun_strext _ _ _ Zm_plus).
proof: Proof. red. intros. elim (Zmodeq_dec m x1 x2). elim (Zmodeq_dec m y1 y2). intros Hyeq Hxeq. elim X. auto with zarith. intros Hyneq _. right. intro Hyeq. elim Hyneq. exact Hyeq. intros Hxneq. left. intro Hxeq. elim Hxneq. exact Hxeq. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields