let EVEN_DIV_LEM = 
prove_by_refinement(
  `!set p q c d a n. 
     (!x. a pow n * p x = c x * q x + d x) ==> 
     a <> &0 ==> 
     EVEN n ==>               
       ((interpsign set q Zero) ==> 
        (interpsign set d Neg)  ==> 
         (interpsign set p Neg)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set d Pos)  ==> 
         (interpsign set p Pos)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set d Zero)  ==> 
         (interpsign set p Zero))`,

(* {{{ Proof *)

[
  REWRITE_TAC[interpsign];
  REPEAT STRIP_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `&0 < a pow n`; 
  ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `&0 < a pow n`; 
  ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  STRIP_TAC;
  CLAIM `a pow n * p x > &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `&0 < a pow n`; 
  ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  STRIP_TAC;
  CLAIM `a pow n * p x = &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_POS_NZ];
]);;
(* }}} *)

let GT_DIV_LEM = 
prove_by_refinement(
  `!set p q c d a n. 
     (!x. a pow n * p x = c x * q x + d x) ==> 
     a > &0 ==> 
       ((interpsign set q Zero) ==> 
        (interpsign set d Neg)  ==> 
         (interpsign set p Neg)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set d Pos)  ==> 
         (interpsign set p Pos)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set d Zero)  ==> 
         (interpsign set p Zero))`,

(* {{{ Proof *)
[
  REWRITE_TAC[interpsign];
  REPEAT_N 9 STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[REAL_POW_LT;real_gt;];
  STRIP_TAC;
  REPEAT STRIP_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  (* save *) 
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x > &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x = &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
]);;
(* }}} *)

let NEG_ODD_LEM = 
prove_by_refinement(
  `!set p q c d a n. 
     (!x. a pow n * p x = c x * q x + d x) ==> 
     a < &0 ==>
     ODD n ==>  
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. -- d x) Neg)  ==> 
         (interpsign set p Neg)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. -- d x) Pos)  ==> 
         (interpsign set p Pos)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. -- d x) Zero)  ==> 
         (interpsign set p Zero))`,

(* {{{ Proof *)
[
  REWRITE_TAC[interpsign;POLY_NEG];
  REPEAT_N 10 STRIP_TAC;
  CLAIM `a pow n < &0`;
  ASM_MESON_TAC[PARITY_POW_LT;real_gt;];
  STRIP_TAC;
  REAL_SIMP_TAC;
  REPEAT STRIP_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x > &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  (* save *) 
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `a pow n * p x = &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
]);;
(* }}} *)

let NEQ_ODD_LEM = 
prove_by_refinement(
  `!set p q c d a n. 
     (!x. a pow n * p x = c x * q x + d x) ==> 
     a <> &0 ==>
     ODD n ==>  
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. a * d x) Neg)  ==> 
         (interpsign set p Neg)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. a * d x) Pos)  ==> 
         (interpsign set p Pos)) /\ 
       ((interpsign set q Zero) ==> 
        (interpsign set (\x. a * d x) Zero)  ==> 
         (interpsign set p Zero))`,

(* {{{ Proof *)
[
  REWRITE_TAC[interpsign;POLY_CMUL];
  REPEAT_N 10 STRIP_TAC;
  CLAIM `a < &0 \/ a > &0 \/ (a = &0)`;
  REAL_ARITH_TAC;
  REWRITE_ASSUMS[NEQ];
  ASM_REWRITE_TAC[];
  LABEL_ALL_TAC;
  STRIP_TAC;
  (* save *) 
  CLAIM `a pow n < &0`;
  ASM_MESON_TAC[PARITY_POW_LT];
  STRIP_TAC;
  REPEAT STRIP_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x > &0`;
  POP_ASSUM MP_TAC;
  ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  REWRITE_TAC[REAL_MUL_LT];
  REPEAT STRIP_TAC;
  CLAIM `&0 < a pow n * p x`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_GT];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  (* save *) 
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x < &0`;
  POP_ASSUM MP_TAC;
  REWRITE_TAC[REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x = &0`;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
  STRIP_TAC;
  CLAIM `a pow n * p x = &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
  (* save *) 
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[EVEN_ODD_POW;NEQ;real_gt];
  STRIP_TAC;
  REPEAT STRIP_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x < &0`;
  POP_ASSUM MP_TAC;
  ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  REWRITE_TAC[REAL_MUL_LT];
  REPEAT STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  (* save *) 
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x > &0`;
  POP_ASSUM MP_TAC;
  REWRITE_TAC[REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  CLAIM `a pow n * p x < &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  STRIP_TAC;
  CLAIM `a pow n * p x > &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  REPEAT STRIP_TAC;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  STRIP_TAC;
  CLAIM `d x = &0`;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
  STRIP_TAC;
  CLAIM `a pow n * p x = &0`;
  EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
]);;
(* }}} *)

let NEQ_MULT_LT_LEM = 
prove_by_refinement(
  `!a q d d' set. 
     a < &0 ==>
       ((interpsign set d Neg)  ==> 
        (interpsign set (\x. a * d x) Pos)) /\ 
       ((interpsign set d Pos)  ==> 
         (interpsign set (\x. a * d x) Neg)) /\ 
       ((interpsign set d Zero)  ==> 
         (interpsign set (\x. a * d x) Zero))`,

(* {{{ Proof *)
[
  REWRITE_TAC[interpsign;POLY_NEG];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_MUL_GT;real_gt];  
  ASM_MESON_TAC[REAL_MUL_LT;real_gt];  
  ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
]);;
(* }}} *)

let NEQ_MULT_GT_LEM = 
prove_by_refinement(
  `!a q d d' set. 
     a > &0 ==>
       ((interpsign set d Neg)  ==> 
         (interpsign set (\x. a * d x) Neg)) /\ 
       ((interpsign set d Pos)  ==> 
         (interpsign set (\x. a * d x) Pos)) /\ 
       ((interpsign set d Zero)  ==> 
         (interpsign set (\x. a * d x) Zero))`,

(* {{{ Proof *)
[
  REWRITE_TAC[interpsign;POLY_NEG] THEN 
  MESON_TAC[REAL_MUL_LT;REAL_ENTIRE;REAL_NOT_EQ;REAL_MUL_GT;real_gt];  
]);;
(* }}} *)

let unknown_thm = 
prove(
  `!set p. (interpsign set p Unknown)`,

    MESON_TAC[interpsign]);;
let ips_gt_nz_thm = 
prove_by_refinement(
  `!x. x > &0 ==> x <> &0`,

(* {{{ Proof *)
[
  REWRITE_TAC[NEQ];
  REAL_ARITH_TAC;
]);;
(* }}} *)

let ips_lt_nz_thm = 
prove_by_refinement(
  `!x. x < &0 ==> x <> &0`,

(* {{{ Proof *)
[
  REWRITE_TAC[NEQ];
  REAL_ARITH_TAC;
]);;
(* }}} *)