# [isabelle] cancel group.

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] cancel group.
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Fri, 05 Nov 2010 12:34:26 +0200
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.12) Gecko/20101027 Lightning/1.0b2 Thunderbird/3.1.6

Hello,

`Is there a reason for the following specification of not being part of
``the Isabelle library?
`
context group_add
begin;
subclass cancel_semigroup_add;
proof
fix a b c :: 'a
assume "a + b = a + c"
then have "- a + a + b = - a + a + c"
unfolding add_assoc by simp
then show "b = c" by simp
next;
fix a b c :: 'a
assume "b + a = c + a"
then have "b + a + - a = c + a + - a" by simp;
then show "b = c" unfolding add_assoc; by simp;
qed;
end;
Best regards,
Viorel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*