proposition: Lemma Comp_MonMor_op_law : MonOp_law Comp_MonMor_map.
proof: Proof. unfold MonOp_law, Comp_MonMor_map in |- *. simpl in |- *; unfold Comp_fun in |- *. intros a b. apply Trans with (g (f a +_M f b)). apply (Pres g); apply MMon_op. apply MMon_op. Qed.
imports: SET Monoid