proposition: Theorem g_cancel_r: forall (g : FGroup op), forall a b c, In a g.(s) -> In b g.(s) -> In c g.(s) -> op b a = op c a -> b = c.
proof: Proof. intros g a b c H1 H2 H3 H4; apply trans_equal with (op b g.(e)); sauto. replace (g.(e)) with (op a (g.(i) a)); sauto. apply trans_equal with (op (op b a) (i g a)); sauto. apply assoc with g; auto. rewrite H4. apply trans_equal with (op c (op a (i g a))); sauto. apply sym_equal; apply assoc with g; sauto. replace (op a (g.(i) a)) with g.(e); sauto. Qed.
imports: List UList Tactic ZArith