```>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
```