(* 1 *)  DefineTerm "Three" "One + One + One" []; 
(* 2 *) 

(* 1 *)  Start "a1 < a1 + One"; 
(* 2 *)  ThmCut "ZEROLESSONE"; 
(* 3 *)  ThmCut "MPLUS"; 
(* 4 *)  l(); Done(); 
(* 6 *)  su 4 "a1"; ThmCut "CPLUS"; 
(* 8 *)  rwl 2; ThmCut "IPLUSa"; 
(* 10 *)  su 7 "a1 + One"; gl2 3; crwl ~1; ThmCut "CPLUS"; 
(* 14 *)  gl2 3; rwl 1; UseThm "LESSTYPEa" [2] [1]; 
(* 17 *)  UseThm "RPLUS" [] [1]; 

(* 18

SOMETHINGBIGGER:



|-

1:  a1 < a1 + One


*)

NameSequent 1 "SOMETHINGBIGGER"; 
(* 20 *) 



DefineTerm "Two" "One + One" []; 
(* 2 *)  

(* 2 *)  DefineTerm "Half" "Inv(Two)" []; 

(* 1 *)  Start "Real(Two)"; 
(* 2 *)  Cut "One + One = Two"; 
(* 3 *)  crwr 1; UseThm "RPLUS" [] [1]; 
(* 5 *)  DefEquals(); Reflexiveeq(); 
(* 7 *)  

(* 6

RTWO:



|-

1:  Real(Two)


*)

NameSequent 1 "RTWO"; 
(* 8 *)  


(* 1 *)  Start "Real(Half)"; 
(* 2 *)  Cut "Half = Inv(Two)"; 
(* 3 *)  rwr 1; UseThm "RINV" [] [1]; 
(* 5 *)  DefEquals(); Reflexiveeq(); 
(* 7 *)  

(* 6

RHALF:



|-

1:  Real(Half)


*)

NameSequent 1 "RHALF"; 
(* 8 *)  


(* 1 *)  Start "Zero < Two"; 
(* 2 *)  DefEquals(); DefEquals(); r(); ThmCut "ZEROLESSONE"; 
(* 6 *)  ThmCut "MPLUS"; 
(* 7 *)  Undo(); ThmCut "SOMETHINGBIGGER"; 
(* 9 *)  su 4 "One"; ThmCut "TRANS"; 
(* 11 *)  l(); r(); gl 2; gr 1; Done(); 
(* 16 *)  Done(); 
(* 17 *)  Cut "One + One = Two"; 
(* 18 *)  crwr 1; gl 2; gr 1; Done(); 
(* 22 *)  DefEquals(); Reflexiveeq(); 
(* 24 *)  

(* 23

TWOPOS:



|-

1:  Zero < Two


*)

NameSequent 1 "TWOPOS"; 
(* 25 *)  



(* 1 *)  Start "Zero < Half"; 
(* 2 *)  ThmCut "TWOPOS"; 
(* 3 *)  ThmCut "POSINV"; 
(* 4 *)  Cut "Inv(Two) = Half"; 
(* 5 *)  rwl 1; gl 2; gr 1; Done(); 
(* 9 *)  DefEquals(); Reflexiveeq(); 
(* 11 *)  Done(); 
(* 12 *)  

(* 11

HALFPOS:



|-

1:  Zero < Half


*)

NameSequent 1 "HALFPOS"; 
(* 13 *)  

(* 1 *)  Start "Half + Half = One"; 
(* 2 *)  ThmCut "ITIMES"; 
(* 3 *)  l(); UseThm "RHALF" [] [1]; 
(* 5 *)  crwr ~1; ThmCut "DIST"; 
(* 7 *)  crwr 1; DefEquals(); Undo(); Cut "One + One = Two"; 
(* 11 *)  rwr 1; Cut "Half = Inv(Two)"; 
(* 13 *)  rwr 1; ThmCut "CTIMES"; 
(* 15 *)  rwr 1; ThmCut "INV"; 
(* 17 *)  l(); NextGoal(); 
(* 19 *)  NextGoal(); 
(* 20 *)  NextGoal(); 
(* 21 *)  NextGoal(); 
(* 22 *)  Done(); 
(* 23 *)  ThmCut "TWOPOS"; 
(* 50 *)  UseThm "NOTBOTH3" [1,2] []; 
(* 51 *)  DefEquals(); Reflexiveeq(); 
(* 53 *)  DefEquals(); Reflexiveeq(); 
(* 55 *)  

(* 54

TWOHALVES:



|-

1:  Half + Half = One


*)

NameSequent 1 "TWOHALVES"; 
(* 56 *)  

(* 1 *)  Start "Zero < a1 -> Zero < Half*a1"; 
(* 2 *)  r(); ThmCut "MTIMES"; 
(* 5 *)  l(); r(); UseThm "HALFPOS" [] [1]; 
(* 8 *)  Done(); 
(* 9 *)  ThmCut "MZERO2"; 
(* 10 *)  rwl 1; ThmCut "CTIMES"; 
(* 12 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 17 *)  

(* 16

MHALFPOS:

1:  Zero < a1


|-

1:  Zero < Half * a1


*)

NameSequent 2 "MHALFPOS"; 
(* 18 *)  


(* 1 *)  Start "Zero < a1 & Real(a1) -> Half*a1 < a1"; 
(* 2 *)  r(); l(); Cut "Zero < Half*a1"; 
(* 5 *)  ThmCut "MPLUS"; 
(* 6 *)  l(); Done(); 
(* 8 *)  su 4 "Half*a1"; ThmCut "IPLUSa"; 
(* 10 *)  ThmCut "CPLUS"; 
(* 11 *)  rwl 1; gl 2; rwl 1; ThmCut "DIST2"; 
(* 15 *)  gl2 3; crwl 1; ThmCut "TWOHALVES"; 
(* 18 *)  gl2 3; rwl 1; ThmCut "ITIMES"; 
(* 21 *)  l(); gl 5; gr 1; Done(); 
(* 25 *)  ThmCut "CTIMES"; 
(* 26 *)  rwl 1; gl 2; gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 33 *)  UseThm "RTIMES" [] [1]; 
(* 34 *)  UseThm "MHALFPOS" [1] [1]; 
(* 35 *)  

(* 34

HalfLess:

1:  Zero < a1
2:  Real(a1)


|-

1:  Half * a1 < a1


*)

NameSequent 3 "HalfLess"; 
(* 36 *) 

(* 1 *)  Start "Zero < a1 -> Zero < a1*a1"; 
(* 2 *)  r(); ThmCut "MTIMES"; 
(* 4 *)  l(); r(); Done(); 
(* 7 *)  Done(); 
(* 8 *)  ThmCut "MZERO2"; 
(* 9 *)  rwl 1; gl 2; gr 1; Done(); 
(* 13 *)  

(* 12

SQPOS:

1:  Zero < a1


|-

1:  Zero < a1 * a1


*)

NameSequent 2 "SQPOS"; 
(* 14 *) 



(* 1 *)  Start "Zero < a1 & Zero < a2 -> (a1<a2 == a1*a1<a2*a2)"; 
(* 2 *)  r(); r(); l(); r(); r(); ThmCut "MTIMES"; 
(* 8 *)  l(); r(); gl 3; gr 1; Done(); 
(* 13 *)  Done(); 
(* 14 *)  ThmCut "MTIMES"; 
(* 15 *)  l(); r(); gl 3; gr 1; Done(); 
(* 20 *)  gl 2; gr 1; Done(); 
(* 23 *)  ThmCut "CTIMES"; 
(* 24 *)  rwl 2; ThmCut "TRANS"; 
(* 26 *)  l(); r(); gl 2; gr 1; Done(); 
(* 31 *)  gl 3; gr 1; Done(); 
(* 34 *)  Done(); 
(* 35 *)  r(); 
(* 37 *)  l();  l(); ThmCut "TRI"; 
(* 48 *)  l(); su 14 "a1"; su 15 "a2"; l(); ThmCut "SubLemma"; 
(* 53 *)  gl2 3; rwl 1; ThmCut "SubLemma"; 
(* 56 *)   gl2 3;  rwl 2; ThmCut "CTIMES"; 
(* 63 *)  gl2 3; rwl 1; ThmCut "CTIMES"; 
(* 66 *)  gl2 3; rwl 2; ThmCut "SubLemma"; 
(* 69 *)  gl2 3; rwl 1; ThmCut "SubLemma"; 
(* 72 *)  gl2 3; rwl 2; gl 5; gl2 8; rwl ~1; gl 10; gl2 3; crwl ~1; gl 8; gl2 5; crwl ~1; gl 6; gl2 7; crwl ~1; ThmCut "IRR"; 
(* 89 *)  l(); gl 2; gr 1; Done(); 
(* 93 *)  l(); Done(); 
(* 95 *)  ThmCut "SquareOrder1"; 
(* 96 *)   UseThm "NOTBOTH" [1,3] []; 
(* 101 *)  Done(); 
(* 102 *)  gl 4; gr 1; Done(); 
(* 105 *)  gl 3; gr 1; Done(); 
(* 108 *)  

NameSequent 29 "SquareOrder2";





(* 1 *)  Start "Real(One)"; 
(* 2 *)  Cut "One = Two*Half"; 
(* 3 *)  rwr 1; UseThm "RTIMES" [] [1]; 
(* 5 *)  Cut "Half = Inv(Two)"; 
(* 6 *)  rwr 1; ThmCut "INV"; 
(* 8 *)  l(); NextGoal(); 
(* 10 *)  NextGoal(); 
(* 11 *)  ThmCut "CTIMES"; 
(* 12 *)  rwl 1; gl 2; gl 3; rwr 1; gl 2; rwr 1; Reflexiveeq(); 
(* 19 *)  ThmCut "TWOPOS"; 
(* 20 *)  UseThm "NOTBOTH3" [1,2] []; 
(* 21 *)  DefEquals(); Reflexiveeq(); 
(* 23 *)  

(* 22

RONE:



|-

1:  Real(One)


*)

NameSequent 1 "RONE"; 
(* 24 *) 


(* 1 *)  Start "Zero < a1 & Real(a1) -> a1 < [a1 +One]*[a1 +One]"; 
(* 2 *)  r(); l(); ThmCut "MPLUS"; 
(* 5 *)  l(); Done(); 
(* 7 *)  su 4 "One"; ThmCut "IPLUSb"; 
(* 9 *)  rwl 1; pl 1; ThmCut "MTIMES"; 
(* 12 *)  l(); r(); gl 2; gr 1; Done(); 
(* 17 *)  Done(); 
(* 18 *)  ThmCut "ITIMES"; 
(* 19 *)  l(); gl 4; gr 1; Done(); 
(* 23 *)  ThmCut "CTIMES"; 
(* 24 *)  rwl 1; pl 1; rwl 1; pl 1; ThmCut "SOMETHINGBIGGER"; 
(* 29 *)  su 12 "a1"; ThmCut "MTIMES"; 
(* 31 *)  l(); r(); su 15 "a1+One"; ThmCut "TRANS"; 
(* 35 *)  l(); r(); gl 4; gr 1; Done(); 
(* 40 *)  Done(); 
(* 41 *)  Done(); 
(* 42 *)  Done(); 
(* 43 *)  ThmCut "CTIMES"; 
(* 44 *)  rwl 1; pl 1; ThmCut "TRANS"; 
(* 47 *)  l(); r(); gl 3; gr 1; Done(); 
(* 52 *)  Done(); 
(* 53 *)  Done(); 
(* 54 *)  UseThm "RONE" [] [1]; 
(* 55 *)  

(* 54

SqLemma:

1:  Zero < a1
2:  Real(a1)


|-

1:  a1 < [a1 + One] * [a1 + One]


*)

NameSequent 3 "SqLemma"; 
(* 56 *)  

(* 1 *)  Start "Zero<=a1 & Real(a1) &Zero<a2&Real(a2)& (Ax1.Real(x1)&Zero<x1 & x1<a2 -> a1 <= x1)-> Zero = a1"; 
(* 2 *)  r(); l(); gl 2; l(); gl 2; l(); gl 2; l(); gl 3; l(); l(); ThmCut "EQUALITY"; 
(* 14 *)  Done(); 
(* 15 *)  Done(); 
(* 16 *)  UseThm "RZERO" [] [1]; 
(* 17 *)  gl 2; gr 1; Done(); 
(* 20 *)  gl 5; w "Half*a1"; 
(* 22 *)  l(); r(); UseThm "RTIMES" [] [1]; 
(* 25 *)  r(); UseThm "MHALFPOS" [2] [1]; 
(* 27 *)  Cut "a1 < a2"; 
(* 28 *)  ThmCut "HalfLess"; 
(* 29 *)  su 5 "a1"; ThmCut "TRANS"; 
(* 31 *)  l(); r(); Done(); 
(* 34 *)  gl 2; gr 1; Done(); 
(* 37 *)  Done(); 
(* 38 *)  gl 3; gr 1; Done(); 
(* 41 *)  gl 4; gr 1; Done(); 
(* 44 *)  w "Half*a2"; 
(* 45 *)  l(); r(); UseThm "RTIMES" [] [1]; 
(* 48 *)  r(); UseThm "MHALFPOS" [4] [1]; 
(* 50 *)  UseThm "HalfLess" [4,5] [1]; 
(* 51 *)  l(); l(); ThmCut "EQUALITY"; 
(* 54 *)  su 9 "a1"; su 10 "Half*a2"; rwl 1; Undo(); rwr 1; UseThm "HalfLess" [6,7] [1]; 
(* 60 *)  Done(); 
(* 61 *)  gl 4; gr 1; Done(); 
(* 64 *)  UseThm "RTIMES" [] [1]; 
(* 65 *)  ThmCut "HalfLess"; 
(* 66 *)  su 11 "a2"; ThmCut "TRANS"; 
(* 68 *)  l(); r(); gl 2; gr 1; Done(); 
(* 73 *)  Done(); 
(* 74 *)  Done(); 
(* 75 *)  gl 5; gr 1; Done(); 
(* 78 *)  gl 6; gr 1; Done(); 
(* 81 *)  l(); l(); ThmCut "HalfLess"; 
(* 84 *)  su 15 "a1"; UseThm "NOTBOTH3" [1,2] []; 
(* 86 *)  gl 3; gr 1; Done(); 
(* 89 *)  gl 4; gr 1; Done(); 
(* 92 *)  ThmCut "HalfLess"; 
(* 93 *)  su 16 "a1"; UseThm "NOTBOTH" [1,2] []; 
(* 95 *)  gl 3; gr 1; Done(); 
(* 98 *)  gl 4; gr 1; Done(); 
(* 101 *)  

(* 100

EPSLEMMA:

1:  Zero <= a1
2:  Real(a1)
3:  Zero < a2
4:  Real(a2)
5:  (Ax1.
     Real(x1) & Zero < x1 & x1 < a2 -> a1 <= x1)


|-

1:  Zero = a1


*)

NameSequent 6 "EPSLEMMA"; 
(* 102 *)    



(* 1 *)  Start "[a1+a2]*[a1+a2] = a1*a1 + Two*a1*a2 + a2*a2"; 
(* 2 *)  Cut "Two*a1*a2 = a1*a2 + a1*a2"; 
(* 3 *)  rwr 1; ThmCut "APLUS"; 
(* 5 *)  rwr 1; ThmCut "APLUS"; 
(* 7 *)  crwr 1; ThmCut "DIST"; 
(* 9 *)  crwr 1; ThmCut "DIST2"; 
(* 11 *)  crwr 1; ThmCut "CTIMES"; 
(* 13 *)  rwr 2; ThmCut "DIST"; 
(* 15 *)  crwr 1; Reflexiveeq(); 
(* 17 *)  Cut "Two = One + One"; 
(* 18 *)  rwr 1; ThmCut "DIST2"; 
(* 20 *)  rwr 1; ThmCut "CTIMES"; 
(* 22 *)  rwr ~1; ThmCut "ITIMES"; 
(* 24 *)  l(); NextGoal(); 
(* 26 *)  DefEquals(); Reflexiveeq(); 
(* 28 *)  rwr ~1; Reflexiveeq(); 
(* 30 *)  UseThm "RTIMES" [] [1]; 
(* 31 *)  

(* 30

FOIL:



|-

1:  [a1 + a2] * [a1 + a2] = a1 * a1 + 
     Two * a1 * a2
      + a2 * a2


*)

NameSequent 1 "FOIL"; 
(* 32 *)  

 

(* 1 *)  Start "Real(a1) & Zero < a1 -> (Ex2.x2 E {x3| Zero < x3 & x3*x3 <a1})"; 
(* 2 *)  r(); l(); ThmCut "TRI"; 
(* 5 *)  su 2 "a1"; su 3 "One"; l(); ThmCut "EQUALITY"; 
(* 9 *)  NextGoal(); 
(* 10 *)  NextGoal(); 
(* 11 *)  Done(); 
(* 12 *)  gl 2; gr 1; Done(); 
(* 15 *)  UseThm "RONE" [] [1]; 
(* 16 *)  w "Half*a1"; 
(* 17 *)  r(); r(); UseThm "MHALFPOS" [4] [1]; 
(* 20 *)  rwr ~1; ThmCut "ITIMES"; 
(* 22 *)  l(); NextGoal(); 
(* 24 *)  NextGoal(); 
(* 25 *)  rwr ~1; Cut "Half < Two"; 
(* 27 *)  ThmCut "MTIMES"; 
(* 28 *)  l(); r(); NextGoal(); 
(* 31 *)  NextGoal(); 
(* 32 *)  NextGoal(); 
(* 33 *)  NextGoal(); 
(* 34 *)  NextGoal(); 
(* 35 *)  NextGoal(); 
(* 36 *)  NextGoal(); 
(* 37 *)  NextGoal(); 
(* 38 *)  NextGoal(); 
(* 39 *)  NextGoal(); 
(* 40 *)  NextGoal(); 
(* 41 *)  NextGoal(); 
(* 42 *)  NextGoal(); 
(* 43 *)  NextGoal(); 
(* 44 *)  NextGoal(); 
(* 45 *)  NextGoal(); 
(* 46 *)  Done(); 
(* 47 *)  UseThm "HALFPOS" [] [1]; 
(* 48 *)  Cut "Two*Half = One"; 
(* 49 *)  crwr 1; gl 2; gr 1; Done(); 
(* 53 *)  Cut "Half = Inv(Two)"; 
(* 54 *)  rwr 1; ThmCut "INV"; 
(* 56 *)  l(); NextGoal(); 
(* 58 *)  NextGoal(); 
(* 59 *)  NextGoal(); 
(* 60 *)  NextGoal(); 
(* 61 *)  NextGoal(); 
(* 62 *)  NextGoal(); 
(* 63 *)  NextGoal(); 
(* 64 *)  NextGoal(); 
(* 65 *)  DefEquals(); Reflexiveeq(); 
(* 67 *)  rwr 1; Reflexiveeq(); 
(* 69 *)  ThmCut "TWOPOS"; 
(* 70 *)  UseThm "NOTBOTH3" [1,2] []; 
(* 71 *)  ThmCut "HalfLess"; 
(* 72 *)  su 11 "One"; gl 2; gl2 6; rwl 1; Cut "One < Two"; 
(* 77 *)  ThmCut "TRANS"; 
(* 78 *)  l(); r(); gl 3; gr 1; Done(); 
(* 83 *)  Done(); 
(* 84 *)  Done(); 
(* 85 *)  ThmCut "ZEROLESSONE"; 
(* 86 *)  ThmCut "MPLUS"; 
(* 87 *)  l(); Done(); 
(* 89 *)  su 17 "One"; ThmCut "IPLUSb"; 
(* 91 *)  rwl 1; Cut "One + One = Two"; 
(* 93 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 98 *)  DefEquals(); Reflexiveeq(); 
(* 100 *)  UseThm "RONE" [] [1]; 
(* 101 *)  UseThm "ZEROLESSONE" [] [1]; 
(* 102 *)  UseThm "RONE" [] [1]; 
(* 103 *)  UseThm "RHALF" [] [1]; 
(* 104 *)  l(); w "Half*a1"; 
(* 106 *)  r(); r(); UseThm "MHALFPOS" [3] [1]; 
(* 109 *)  ThmCut "MTIMES"; 
(* 110 *)  l(); r(); gl 3; gr 1; Done(); 
(* 115 *)  Done(); 
(* 116 *)  ThmCut "ITIMES"; 
(* 117 *)  l(); NextGoal(); 
(* 119 *)  NextGoal(); 
(* 120 *)  ThmCut "CTIMES"; 
(* 121 *)  rwl 1; gl 2; rwl 1; Cut "Zero < Half"; 
(* 125 *)  ThmCut "MTIMES"; 
(* 126 *)  l(); r(); Done(); 
(* 129 *)  gl 3; gr 1; Done(); 
(* 132 *)  Cut "a1*Half <a1"; 
(* 133 *)  ThmCut "TRANS"; 
(* 134 *)  l(); r(); gl 2; gr 1; Done(); 
(* 139 *)  Done(); 
(* 140 *)  ThmCut "MTIMES"; 
(* 141 *)  l(); r(); gl 4; gr 1; Done(); 
(* 146 *)  Done(); 
(* 147 *)  ThmCut "TRANS"; 
(* 148 *)  l(); r(); Done(); 
(* 151 *)  gl 3; gr 1; Done(); 
(* 154 *)  ThmCut "CTIMES"; 
(* 155 *)  rwl ~1; ThmCut "ATIMES"; 
(* 157 *)  gl2 3; rwl 1; ThmCut "CTIMES"; 
(* 160 *)  gl2 3; rwl 1; Undo(); rwl 4; ThmCut "ATIMES"; 
(* 165 *)  rwr ~1; gl 3; gr 1; Done(); 
(* 169 *)  ThmCut "CTIMES"; 
(* 170 *)  rwr 1; UseThm "HalfLess" [8,7] [1]; 
(* 172 *)  UseThm "HALFPOS" [] [1]; 
(* 173 *)  gl 3; gr 1; Done(); 
(* 176 *)  w "One"; 
(* 177 *)  r(); r(); UseThm "ZEROLESSONE" [] [1]; 
(* 180 *)  ThmCut "ITIMES"; 
(* 181 *)  l(); NextGoal(); 
(* 183 *)  rwr 1; gl 2; gr 1; Done(); 
(* 187 *)  UseThm "RONE" [] [1]; 
(* 188 *)  

(* 187

SupLemma:

1:  Real(a1)
2:  Zero < a1


|-

1:  (Ex2.x2 E {x3|Zero < x3 & x3 * x3 < a1})


*)

NameSequent 3 "SupLemma"; 
(* 189 *)  


(* 1 *)  Start "Half*Two = One"; 
(* 2 *)  Cut "Half = Inv(Two)"; 
(* 3 *)  rwr 1; ThmCut "CTIMES"; 
(* 5 *)  rwr 1; ThmCut "INV"; 
(* 7 *)  l(); NextGoal(); 
(* 9 *)  Done(); 
(* 10 *)  NextGoal(); 
(* 11 *)  Done(); 
(* 12 *)  ThmCut "TWOPOS"; 
(* 13 *)  UseThm "NOTBOTH3" [1,2] []; 
(* 14 *)  DefEquals(); Reflexiveeq(); 
(* 16 *)  

(* 15

HALFTWO:



|-

1:  Half * Two = One


*)

NameSequent 1 "HALFTWO"; 
(* 17 *)  



(* 1 *)  Start "Zero < a1 & a1 < a2 -> a1*a1+Two*a1*a2+a2*a2 < a1*a2+Two*a1*a2+a2*a2"; 
(* 2 *)  r(); l(); ThmCut "MTIMES"; 
(* 5 *)  l(); r(); Done(); 
(* 8 *)  gl 2; gr 1; Done(); 
(* 11 *)  ThmCut "MPLUS"; 
(* 12 *)  l(); Done(); 
(* 14 *)  su 8 "Two * a1*a2 + a2*a2"; ThmCut "CTIMES"; 
(* 16 *)  rwl 8; Undo(); rwl 16; gl 2; gr 1; Done(); 
(* 22 *)  

(* 21

ORDERLEMMA1:

1:  Zero < a1
2:  a1 < a2


|-

1:  a1 * a1 + Two * a1 * a2 + a2
      * a2 < a1 * a2
      + Two * a1
      * a2 + a2 * a2


*)

NameSequent 3 "ORDERLEMMA1"; 
(* 23 *)  


(* 1 *)  Start "Zero < Three"; 
(* 2 *)  ThmCut "ZEROLESSONE"; 
(* 3 *)  ThmCut "MPLUS"; 
(* 4 *)  l(); Done(); 
(* 6 *)  su 3 "One"; ThmCut "IPLUSb"; 
(* 8 *)  rwl 1; ThmCut "TRANS"; 
(* 10 *)  l(); r(); gl 3; gr 1; Done(); 
(* 15 *)  gl 2; gr 1; Done(); 
(* 18 *)  ThmCut "MPLUS"; 
(* 19 *)  l(); Done(); 
(* 21 *)  su 10 "One"; ThmCut "IPLUSb"; 
(* 23 *)  rwl 1; ThmCut "TRANS"; 
(* 25 *)  l(); r(); gl 6; gr 1; Done(); 
(* 30 *)  gl 2; gr 1; Done(); 
(* 33 *)  ThmCut "APLUS"; 
(* 34 *)  rwl 1; Cut "Three = One+One+One"; 
(* 36 *)  rwl 1; Undo(); rwr 1; gl 3; gr 1; Done(); 
(* 42 *)  DefEquals(); Reflexiveeq(); 
(* 44 *)  UseThm "RONE" [] [1]; 
(* 45 *)  UseThm "RONE" [] [1]; 
(* 46 *)  

(* 45

THREEPOS:



|-

1:  Zero < Three


*)

NameSequent 1 "THREEPOS"; 
(* 47 *) 


(* 1 *)  Start "Zero <a1 & Zero <a2 -> Zero < a1*a2"; 
(* 2 *)  r(); l(); ThmCut "MTIMES"; 
(* 7 *)  l(); r(); Done(); 
(* 10 *)  gl 2; gr 1; Done(); 
(* 13 *)  ThmCut "MZERO2"; 
(* 14 *)  rwl 1; ThmCut "CTIMES"; 
(* 16 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 21 *)  

(* 20

TIMESPOS:

1:  Zero < a1
2:  Zero < a2


|-

1:  Zero < a1 * a2


*)

NameSequent 3 "TIMESPOS"; 
(* 22 *)  


(* 1 *)  Start "Real(a1) -> a1 + Two*a1 = Three*a1"; 
(* 2 *)  r(); ThmCut "ITIMES"; 
(* 6 *)  l(); Done(); 
(* 8 *)  crwr 1; ThmCut "CTIMES"; 
(* 10 *)  rwr 1; ThmCut "DIST2"; 
(* 12 *)  crwr 1; Cut "Two = One + One"; 
(* 14 *)  rwr 1; Cut "Three = One + One + One"; 
(* 18 *)  crwr 1; Reflexiveeq(); 
(* 20 *)  DefEquals(); 
(* 22 *)  Reflexiveeq(); 
(* 23 *)  DefEquals(); Reflexiveeq(); 
(* 25 *)  

(* 24

LIKETERMS1:

1:  Real(a1)


|-

1:  a1 + Two * a1 = Three * a1


*)

NameSequent 2 "LIKETERMS1"; 
(* 26 *)