proposition: Lemma Zmult_wd : bin_fun_wd Z_as_CSetoid Z_as_CSetoid Z_as_CSetoid Zmult.
proof: Proof. red in |- *. simpl in |- *. intros x1 x2 y1 y2 H H0. apply (f_equal2 Zmult (x1:=x1) (y1:=x2) (x2:=y1) (y2:=y2)). assumption. assumption. Qed.
imports: CoRN.model.structures.Zsec CoRN.algebra.CSetoidFun