Hi Dan,
I hope these proofs are of interest to you :-). The 'details' of the
proof are contained in 6 separate files:
- 'addcancelable_short' extends 'cancelability' of addition to
inequalities;
- 'MultCancelable' contains the proof that multiplication is
cancelable;
- 'basic_inequalities' contains two 'rules' for
addition/multiplication of an inequality with a natural number;
- 'lt_eq_exclude' and 'LtProp_short' describe the properties of
antisymmetry, irreflexivity and transitivity of '<', as well as the
fact that a<b,a=b,b<a mutually exclude;
- 'Division2r2' contains the actual proof-- also it contains
a "lemma" from which immediately follows that the subsets of odd and
even numbers are disjoint.

Especially in the 'division' proof, I guess some people would prefer
not to have so many 'lemmata' before the actual start of the proof.
But I thought they might be nice to have them at the "top level"
rather than hidden inside premise blocks. And it's rather annoying
when you find that you can't access a result any more since it's
contained in a closed premise block ;-).

Best regards,

Thomas


[Thanks, Thomas! I have uploaded these proofs to the DC Proof
website:

http://www.dcproof.com/addcancelable_short.proof
http://www.dcproof.com/MultCancelable.proof
http://www.dcproof.com/basic_inequalities.proof
http://www.dcproof.com/lt_eq_exclude.proof
http://www.dcproof.com/LtProp_short.proof
http://www.dcproof.com/Division2r2.proof

Dan]