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