Hi Thomas,

Heading in the direction you've suggested:

x<y
=>x+x<y+x
=>x+y<y+y
x+y=y+x
=>x+x<y+y

This requires a<b=>a+c<b+c, a+b=b+a, a<b & b<c => a<c

And if you have [a<b | a=b | b<a] & ~[a<b & a=b] & ~[a=b & b<a] & ~[a<b
& b<a]

that is enough. See http://www.ozemail.com.au/~markhurd/UniqueEven.html
and http://www.ozemail.com.au/~markhurd/UniqueEven.proof

However, you'll need to check the proofs of the above lemmas to see if
they already include something like cancellation or another construct
that makes the implication requested trivial.

Regards,
Mark Hurd, B.Sc.(Ma.) (Hons.)

----- Original Message -----
From: "Thomas Heye" <1910-131@...>
To: <dcproof@yahoogroups.com>
Sent: Saturday, September 16, 2006 3:41 AM
Subject: [DC Proof] Ideas for uniqueness of even number function


> Hi folks,
> I'd like to prove for all natural numbers a,b that a +a=b+b implies
> a=b.
>
> My ideas so far: Having shown that a<b, a=b, b<a are mutually
> exclusive, it should be possible to deduce from a+a=b+b that a<b, b<a
> resp. is impossible, so equality must hold.
>
> Or is there an easier way?
>
> Thanks,
>
> Thomas