>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