+theorem eq_inv_op_x_y_op_inv_y_inv_x:
+ ∀G:Group. ∀x,y:G. (x·y) \sup -1 = y \sup -1 · x \sup -1.
+intros;
+apply (eq_op_x_y_op_z_y_to_eq ? (x·y));
+rewrite > (inv_is_left_inverse ? G);
+rewrite < (op_associative ? G);
+rewrite > (op_associative ? G (y \sup -1));
+rewrite > (inv_is_left_inverse ? G);
+rewrite > (e_is_right_unit ? G);
+rewrite > (inv_is_left_inverse ? G);
+reflexivity.
+qed.
+