proposition: Theorem inv_op: forall (g: FGroup op) a b, In a g.(s) -> In b g.(s) -> g.(i) (op a b) = op (g.(i) b) (g.(i) a).
proof: Proof. intros g a1 b1 H1 H2; apply g_cancel_l with (g := g) (a := op a1 b1); sauto. repeat rewrite g.(assoc); sauto. apply trans_equal with g.(e); sauto. rewrite <- g.(assoc) with (a := a1); sauto. rewrite g.(i_is_inverse_r); sauto. rewrite g.(e_is_zero_r); sauto. Qed.
imports: List UList Tactic ZArith