proposition: Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A).
proof: Proof. unfold associative in |- *. unfold comp_as_bin_op in |- *. intros A f g h. simpl in |- *. unfold eq_fun in |- *. simpl in |- *. intuition. Qed.
imports: CoRN.algebra.CSetoids