(* ------------------------------------------------------------------------- *)
(* Condense subdivision by removing points with no relevant zeros.           *)
(* ------------------------------------------------------------------------- *)

let real_cases = prove(`!x y. x < y \/ (x = y) \/ y < x`,REAL_ARITH_TAC);;

let gt_aux = prove(
  `!x. (x1 < x2 /\ x2 < x3) /\ ((x1 < x /\ x < x2) \/ (x = x2) \/ (x2 < x /\ x < x3)) ==> x1 < x /\ x < x3`,
   REAL_ARITH_TAC);;

let gen_thm = prove_by_refinement(
 `!P x1 x2 x3. 
      (x1 < x3) ==> 
      (!x. x1 < x /\ x < x2 ==> P x) ==> 
      (!x. (x = x2) ==> P x) ==> 
      (!x. x2 < x /\ x < x3 ==> P x) ==> 
        (!x. x1 < x /\ x < x3 ==> P x)`, 
(* {{{ Proof *)

[
  MESON_TAC[real_cases;gt_aux;DE_MORGAN_THM;REAL_NOT_LT;REAL_LE_LT];
]);;

(* }}} *)

let gen_thm_noleft = prove(
 `!P x2 x3. 
      (x2 < x3) ==> 
      (!x. x < x2 ==> P x) ==> 
      (!x. (x = x2) ==> P x) ==> 
      (!x. x2 < x /\ x < x3 ==> P x) ==> 
        (!x. x < x3 ==> P x)`, 
  MESON_TAC[real_cases;gt_aux]);;

let gen_thm_noright = prove(
 `!P x1 x2. 
      (x1 < x2) ==> 
      (!x. x1 < x /\ x < x2 ==> P x) ==> 
      (!x. (x = x2) ==> P x) ==> 
      (!x. x2 < x ==> P x) ==> 
        (!x. x1 < x ==> P x)`, 
  MESON_TAC[real_cases;gt_aux]);;

let gen_thm_noboth = prove(
 `!P Q x2. 
       Q ==>                                      
      (!x. x < x2 ==> P x) ==> 
      (!x. (x = x2) ==> P x) ==> 
      (!x. x2 < x ==> P x) ==> 
        (!x. T ==> P x)`, 
  MESON_TAC[real_cases;gt_aux]);;