proposition: Lemma dprod_strext:(bin_fun_strext (ProdCSetoid M1 M2)(ProdCSetoid M1 M2) (ProdCSetoid M1 M2)dprod).
proof: Proof. unfold bin_fun_strext. intros x1 x2 y1 y2. unfold dprod. case x1. intros a1 a2. case x2. intros b1 b2. case y1. intros c1 c2. case y2. intros d1 d2. simpl. intro H. elim H. clear H. intro H. cut (a1[#]b1 or c1[#]d1). intuition. set (H0:= (@csg_op M1)). unfold CSetoid_bin_op in H0. set (H1:= (@csbf_strext M1 M1 M1 H0)). unfold bin_fun_strext in H1. apply H1. exact H. clear H. intro H. cut (a2[#]b2 or c2[#]d2). intuition. set (H0:= (@csg_op M2)). unfold CSetoid_bin_op in H0. set (H1:= (@csbf_strext M2 M2 M2 H0)). unfold bin_fun_strext in H1. apply H1. exact H. Qed.
imports: CoRN.algebra.CSetoidInc