>PhoX> Sort real.
Sort real defined
>PhoX> Cst Infix[5] x "<" y : real  real  prop.
$< : real  real  prop
>PhoX> Cst Infix[5] x "<=" y : real  real  prop.
$<= : real  real  prop
>PhoX> Cst zero : real.
zero : real
>PhoX> Cst deux : real.
deux : real
>PhoX> Cst Infix[3] x "-" y : real  real  real.
$- : real  real  real
>PhoX> Cst Infix[2] x "/" y : real  real  real.
$/ : real  real  real
>PhoX> Cst abs : real  real.
abs : real  real
>PhoX> def Infix[5] x ">" y = y < x.
$> = \x,y (y < x) : real  real  prop
>PhoX> def continue1 f = x e > zero a > zero y (abs (x - y) < a  abs (f x - f y) < e).

continue1 =
   \f
     x,e
       (e > zero  a > zero  y (abs (x - y) < a  abs (f x - f y) < e))
 : (real  real)  prop
>PhoX> def continue2 f = x e > zero a > zero y (abs (x - y) <= a  abs (f x - f y) <= e).

continue2 =
   \f
     x,e
       (e > zero  a > zero  y (abs (x - y) <= a  abs (f x - f y) <= e))
 : (real  real)  prop
>PhoX> goal
>PhoX>   a,b (a < b  a <= b) 
>PhoX>   a (a > zero  a / deux > zero) 
>PhoX>   a (a > zero  b (b <= a / deux  b < a)) 

>PhoX>   f (continue1 f  continue2 f).
Here is the goal:
goal 1/1
    a,b (a < b  a <= b)  a > zero  a / deux > zero 
        a > zero  b <= (a / deux)  b < a 
        f (continue1 f  continue2 f)

%PhoX% intro F2 F3 F4 f.
1 goal created.

goal 1/1
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue1 f  continue2 f

%PhoX% intros.
2 goals created.

goal 2/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue2 f  continue1 f

goal 1/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue1 f  continue2 f

%PhoX% intros.
1 goal created.

goal 1/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue1 f
    continue2 f

%PhoX% intros.
1 goal created.

goal 1/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue1 f
H0 := e > zero
    a > zero  y (abs (x - y) <= a  abs (f x - f y) <= e)

%PhoX% elim H with x and H0.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero  y (abs (x - y) < a  abs (f x - f y) < e)
    a0 > zero  y (abs (x - y) <= a0  abs (f x - f y) <= e)

%PhoX% left H1.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    a0 > zero  y (abs (x - y) <= a0  abs (f x - f y) <= e)

%PhoX% intro.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    ?1 > zero  y (abs (x - y) <= ?1  abs (f x - f y) <= e)

%PhoX% instance ?1 a / deux.
Here are the goals:
goal 2/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue2 f  continue1 f

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    a / deux > zero  y (abs (x - y) <= a / deux  abs (f x - f y) <= e)

%PhoX% intro.
2 goals created.

goal 2/3
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    y (abs (x - y) <= a / deux  abs (f x - f y) <= e)

goal 1/3
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    a / deux > zero

%PhoX% elim F3.
1 goal created.

goal 1/3
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    a > zero

%PhoX% axiom H1.
0 goal created.

goal 2/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue2 f  continue1 f

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) < a  abs (f x - f y) < e)
    y (abs (x - y) <= a / deux  abs (f x - f y) <= e)

%PhoX% intros.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    abs (f x - f y) <= e

%PhoX% elim F2.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    abs (f x - f y) < e

%PhoX% elim H2.
1 goal created.

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    abs (x - y) < a

%PhoX% elim F4.
2 goals created.

goal 2/3
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    abs (x - y) <= a / deux

goal 1/3
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    a > zero

%PhoX% axiom H1.
0 goal created.

goal 2/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue2 f  continue1 f

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue1 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) < a  abs (f x - f y0) < e)
H3 := abs (x - y) <= a / deux
    abs (x - y) <= a / deux

%PhoX% axiom H3.
0 goal created.

goal 1/1
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
    continue2 f  continue1 f

%PhoX% intros.
1 goal created.

goal 1/1
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue2 f
    continue1 f

%PhoX% intros.
1 goal created.

goal 1/1
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue2 f
H0 := e > zero
    a > zero  y (abs (x - y) < a  abs (f x - f y) < e)

%PhoX% elim H with x and e / deux.
2 goals created.

goal 2/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero  y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    a0 > zero  y (abs (x - y) < a0  abs (f x - f y) < e)

goal 1/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue2 f
H0 := e > zero
    e / deux > zero

%PhoX% elim F3.
1 goal created.

goal 1/2
F2 := a,b (a < b  a <= b)
F3 := a > zero  a / deux > zero
F4 := a > zero  b <= (a / deux)  b < a
H := continue2 f
H0 := e > zero
    e > zero

%PhoX% axiom H0.
0 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero  y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    a0 > zero  y (abs (x - y) < a0  abs (f x - f y) < e)

%PhoX% left H1.
1 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    a0 > zero  y (abs (x - y) < a0  abs (f x - f y) < e)

%PhoX% intro.
1 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    ?2 > zero  y (abs (x - y) < ?2  abs (f x - f y) < e)

%PhoX% intro.
2 goals created.

goal 2/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    y (abs (x - y) < ?2  abs (f x - f y) < e)

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    ?2 > zero

%PhoX% axiom H1.
0 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y (abs (x - y) <= a  abs (f x - f y) <= e / deux)
    y (abs (x - y) < a  abs (f x - f y) < e)

%PhoX% intros.
1 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    abs (f x - f y) < e

%PhoX% elim F4.
2 goals created.

goal 2/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    abs (f x - f y) <= e / deux

goal 1/2
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    e > zero

%PhoX% axiom H0.
0 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    abs (f x - f y) <= e / deux

%PhoX% elim H2.
1 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    abs (x - y) <= a

%PhoX% elim F2.
1 goal created.

goal 1/1
F2 := a0,b (a0 < b  a0 <= b)
F3 := a0 > zero  a0 / deux > zero
F4 := a0 > zero  b <= (a0 / deux)  b < a0
H := continue2 f
H0 := e > zero
H1 := a > zero
H2 := y0 (abs (x - y0) <= a  abs (f x - f y0) <= e / deux)
H3 := abs (x - y) < a
    abs (x - y) < a

%PhoX% axiom H3.
0 goal created.

%PhoX% save th.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
th =
   a,b (a < b  a <= b)  a > zero  a / deux > zero 
     a > zero  b <= (a / deux)  b < a  f (continue1 f  continue2 f)
 : theorem

bye