(cic:/matita/algebra/monoids/magma.con M).
record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group: isSemiGroup M;
+ { is_semi_group:> isSemiGroup M;
e_is_left_unit:
is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
e_is_right_unit:
generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
simplify; fold simplify (op M);
intro; clear H2;
- generalize in match (associative ? (is_semi_group ? (monoid_properties M)));
+ generalize in match (op_associative ? (is_semi_group ? (monoid_properties M)));
intro;
rewrite > H2 in H3; clear H2;
rewrite > H1 in H3;