let empty_mat = 
prove_by_refinement( `interpmat [] [] [[]]`,
(* {{{ Proof *) [ REWRITE_TAC[interpmat;ROL_EMPTY;interpsigns;ALL2;partition_line]; ]);;
(* }}} *) let empty_sgns = [ARITH_RULE `&1 > &0`];;
let monic_isign_lem = 
prove( `(!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Pos ==> interpsign s p Pos) /\ (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Pos ==> interpsign s p Neg) /\ (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Neg ==> interpsign s p Neg) /\ (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Neg ==> interpsign s p Pos) /\ (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Zero ==> interpsign s p Zero) /\ (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Zero ==> interpsign s p Zero)`,
(* {{{ Proof *) REWRITE_TAC[interpsign] THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC (MATCH_MP y x))) THEN POP_ASSUM MP_TAC THEN POP_ASSUM (ASSUME_TAC o GSYM o (ISPEC `x:real`)) THEN ASM_REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_ENTIRE] THEN REAL_ARITH_TAC);;
(* }}} *) let gtpos::ltpos::gtneg::ltneg::gtzero::ltzero::[] = CONJUNCTS monic_isign_lem;;
let main_lem000 = 
prove_by_refinement( `!l n. (LENGTH l = SUC n) ==> 0 < LENGTH l`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[LENGTH]; ARITH_TAC; ARITH_TAC; ]);;
(* }}} *)
let main_lem001 = 
prove_by_refinement( `x <> &0 ==> (LAST l = x) ==> LAST l <> &0`,
[MESON_TAC[]]);;
let main_lem002 = 
prove_by_refinement( `(x <> y ==> x <> y) /\ (x < y ==> x <> y) /\ (x > y ==> x <> y) /\ (~(x >= y) ==> x <> y) /\ (~(x <= y) ==> x <> y) /\ (~(x = y) ==> x <> y)`,
(* {{{ Proof *) [ REWRITE_TAC[NEQ] THEN REAL_ARITH_TAC ]);;
(* }}} *)
let factor_pos_pos = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Pos ==> (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;real_gt]; DISJ2_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt]; ]);;
(* }}} *)
let factor_pos_neg = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Neg ==> (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_LT;real_gt]; DISJ2_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt]; ]);;
(* }}} *)
let factor_pos_zero = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Zero ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_LT;REAL_ENTIRE;real_gt]; ]);;
(* }}} *)
let factor_zero_pos = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Pos ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE]; DISJ1_TAC; ASM_MESON_TAC[POW_0;num_CASES;]; ]);;
(* }}} *)
let factor_zero_neg = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Neg ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE]; DISJ1_TAC; ASM_MESON_TAC[POW_0;num_CASES;]; ]);;
(* }}} *)
let factor_zero_zero = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Zero ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REAL_ARITH_TAC; ]);;
(* }}} *)
let factor_neg_even_pos = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> EVEN k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt]; DISJ2_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT]; ]);;
(* }}} *)
let factor_neg_even_neg = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> EVEN k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt]; DISJ2_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT]; ]);;
(* }}} *)
let factor_neg_even_zero = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> EVEN k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE]; ]);;
(* }}} *)
let factor_neg_odd_pos = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> ODD k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE]; DISJ1_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT]; ]);;
(* }}} *)
let factor_neg_odd_neg = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> ODD k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE]; DISJ1_TAC; ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT]; ]);;
(* }}} *)
let factor_neg_odd_zero = 
prove_by_refinement( `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> ODD k ==> ~(k = 0) ==> (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
(* {{{ Proof *) [ REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y))); POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM); ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE]; ]);;
(* }}} *)