proposition: Lemma direct_product_is_CSemiGroup: (is_CSemiGroup (ProdCSetoid M1 M2) dprod_as_csb_fun).
proof: Proof. unfold is_CSemiGroup. unfold associative. intros x y z. case x. intros x1 x2. case y. intros y1 y2. case z. intros z1 z2. simpl. split. apply CSemiGroup_is_CSemiGroup. apply CSemiGroup_is_CSemiGroup. Qed.
imports: CoRN.algebra.CSetoidInc