proposition: Lemma Zm_mult_strext : (bin_fun_strext _ _ _ Zm_mult).
proof: Proof. red; simpl. unfold ZModap;unfold Zm_mult; simpl. intros x1 x2 y1 y2. intro H. elim (Zmodeq_dec m x1 x2). elim (Zmodeq_dec m y1 y2). intros Hyeq Hxeq. elim H. apply Zmodeq_mult_elim; 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