inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
}.
inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
}.
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
∀G,G'.∀f:morphism G G'.f˜1 = 1.
intros;
apply (eq_op_x_y_op_z_y_to_eq G' (f˜1));
∀G,G'.∀f:morphism G G'.f˜1 = 1.
intros;
apply (eq_op_x_y_op_z_y_to_eq G' (f˜1));