(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Jlxfdmj = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;
open Fektyiy;;



let SCS_M_EQ_0= prove_by_refinement(
` CARD (scs_M s) = 0 /\ is_scs_v39 s 
==> (!i. scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
[
STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC th
THEN ASSUME_TAC th)
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN DICH_TAC (21)
THEN REWRITE_TAC[scs_M]
THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
THEN SUBGOAL_THEN`FINITE
      {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..6`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN GEN_TAC
THEN DICH_TAC(20-3)
THEN ARITH_TAC;

ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC;

MRESA_TAC CARD_EQ_0[`{i | i < scs_k_v39 s /\
        (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
THEN STRIP_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN THAYTHES_TAC 2[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN THAYTHES_TAC (29-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN REAL_ARITH_TAC]);;


let FINITE_SCS_M=prove(`is_scs_v39 s ==> FINITE (scs_M s)`,
REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39;scs_M]
THEN STRIP_TAC
THEN MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..(scs_k_v39 s)`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN DICH_TAC(19-1)
THEN ARITH_TAC);;

let SCS_A_2=prove(`is_scs_v39 s
==> !i. &2<= scs_a_v39 s i (i+1)`,
REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;GSYM ADD1]
THEN RESA_TAC
THEN STRIP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;is_scs_v39;LET_DEF;LET_END_DEF]
THEN THAYTHES_TAC (21-14)[`i MOD k`;`(SUC i) MOD k`][DIVISION;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`]);;


let SCS_M_EQ_1= prove_by_refinement(` scs_M s={x} /\ is_scs_v39 s 
==> (!i. ~(i MOD scs_k_v39 s=x )==> scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
[
STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC th
THEN ASSUME_TAC th)
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN DICH_TAC (21)
THEN REWRITE_TAC[scs_M]
THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
THEN SUBGOAL_THEN`FINITE
      {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..6`
THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN GEN_TAC
THEN DICH_TAC(20-3)
THEN ARITH_TAC;

ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN THAYTHEL_ASM_TAC 1[`x:num`][]
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN DICH_TAC 5
THEN ASM_SIMP_TAC[MOD_LT]
THEN STRIP_TAC
THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN THAYTHES_TAC (31-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN POP_ASSUM MP_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
THEN REAL_ARITH_TAC]);;

let SCS_M_LE_K=prove(` scs_M s={x} 
==> x<scs_k_v39 s`,
REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`x:num`]);;


let JLXFDMJ_concl = `
main_nonlinear_terminal_v11
==>(!s (v:num->real^3) i.
  3< scs_k_v39 s/\ 
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  (  dist(v i,v (i+1)) = &2) /\
  CARD (scs_M s) <= 1 /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
(!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\
  scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1) <= &2 * h0 ==>
   (!j. ~(j MOD scs_k_v39 s IN scs_M s)==>   dist(v j , v(j+1)) = &2))`;;


let JLXFDMJ = prove_by_refinement(
 JLXFDMJ_concl,

[

STRIP_TAC
THEN REPEAT GEN_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC SCS_A_2
THEN RESA_TAC
THEN SUBGOAL_THEN`!i. &2< scs_b_v39 s i (i + 1)`ASSUME_TAC;


GEN_TAC
THEN THAYTHE_TAC 0[`i'`]
THEN THAYTHE_TAC 3[`i'`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;

MP_TAC(ARITH_RULE`CARD (scs_M s)<=1==> CARD (scs_M s) =0 \/ CARD (scs_M s) =1`)
THEN RESA_TAC;



MP_TAC FINITE_SCS_M
THEN RESA_TAC
THEN MRESA_TAC CARD_EQ_0[`scs_M s`]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i<=j \/ j<=i:num`)
THEN RESA_TAC
;


POP_ASSUM MP_TAC
THEN SPEC_TAC (`j:num`,`j:num`)
THEN INDUCT_TAC
;

REWRITE_TAC[ARITH_RULE`i<= 0<=> i=0`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
THEN REPEAT RESA_TAC)
;


STRIP_TAC
THEN MP_TAC(ARITH_RULE`i<= SUC j==> SUC j=i \/ i<=j`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN MP_TAC SCS_M_EQ_0
THEN RESA_TAC
THEN THAYTHEL_ASM_TAC(24-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(25-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
THEN THAYTHEL_ASM_TAC (32-22)[`j`][ARITH_RULE`SUC i= i+1`]
THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`];



POP_ASSUM MP_TAC
THEN ABBREV_TAC`t= i-j:num`
THEN POP_ASSUM MP_TAC
THEN SPEC_TAC (`j:num`,`j:num`)
THEN SPEC_TAC (`t:num`,`t:num`)
THEN INDUCT_TAC
;



REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`i-j=0/\ j<=i ==> j=i:num`)
THEN RESA_TAC;


REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`i-j= SUC t/\ j<=i ==> i- SUC j=t/\ SUC j<= i:num`)
THEN RESA_TAC
THEN THAYTHEL_TAC 4 [`SUC j`][ARITH_RULE`SUC i= i+1/\ (i+1)+1=i+2`]
THEN MP_TAC SCS_M_EQ_0
THEN RESA_TAC
THEN THAYTHEL_ASM_TAC(26-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(27-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
THEN THAYTHEL_ASM_TAC (34-24)[`j`][ARITH_RULE`SUC i= i+1`]
THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`]
;



MP_TAC FINITE_SCS_M
THEN RESA_TAC
THEN MRESAL_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][IN_SING]
THEN MP_TAC SCS_M_EQ_1
THEN RESA_TAC
THEN SUBGOAL_THEN`~(i MOD k=x)` ASSUME_TAC;


STRIP_TAC
THEN DICH_TAC 2
THEN ASM_REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`i MOD k`]
THEN POP_ASSUM MP_TAC
THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`x`;`k`][MOD_LT;ARITH_RULE`3<k==> ~(k=0)`]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
THEN ASM_REWRITE_TAC[ADD1;REAL_ARITH`~(a<b)<=> b<=a`;REAL_ARITH`a<=a`]
;





MP_TAC(ARITH_RULE`~(i MOD k= x)==>  i MOD k< x\/ x< i MOD k`)
THEN RESA_TAC
;




SUBGOAL_THEN `!t. t< i MOD k + k - x ==> dist ((v:num->real^3) (i MOD k+k - t),v ( (i MOD k+k -t) + 1)) = &2`
ASSUME_TAC
;



INDUCT_TAC
;


STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE`a-0=a/\ (1 * k + i MOD k) + 1= 1*k+SUC(i MOD k)/\ i MOD k +k=1*k+ i MOD k`]
THEN DICH_TAC(24-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+i MOD k`;`v:num->real^3`;`(1*k+i MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(i MOD k)`;`v:num->real^3`;`(1*k+SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;` i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;



STRIP_TAC
THEN MP_TAC SCS_M_LE_K
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k ==> t< i MOD k+k-x`)
THEN RESA_TAC
THEN DICH_TAC 3
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`j1= i MOD k + k - (t+1)`
THEN MRESA_TAC Ssrnat.subn_sub[`t`;`k`;`1`]
THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> i MOD k+ k-t=(i MOD k +k-t-1)+1 `)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ADD1;ARITH_RULE`(i+1)+1=i+2`]
THEN STRIP_TAC
THEN THAYTHEL_ASM_TAC(30-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(31-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;

MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
THEN RESA_TAC
;




MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];


MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= i MOD k +k-(t+1) ==>  i MOD k +k-(t+1) = 1*k+ i MOD k-(t+1)/\ i MOD k-(t+1)<k/\ ~(i MOD k - (t + 1) = x)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];





SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;

MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
THEN RESA_TAC
;




MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];


MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x  ==>    (SUC(i MOD k) +k-(t+1)) =(i MOD k +k-(t+1)) +1`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= (SUC(i MOD k) +k-(t+1)) ==>  (i MOD k +k-(t+1))+1 = 1*k+ SUC(i MOD k)-(t+1)/\  (i MOD k +k-(t+1)) +1=(SUC(i MOD k) +k-(t+1)) /\ SUC(i MOD k)-(t+1)<k/\ ~(i MOD k - t = x) `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
THEN ASM_REWRITE_TAC[ADD1;SUB_ADD_RCANCEL];


THAYTHEL_ASM_TAC (40-19)[`j1`][ARITH_RULE`SUC i= i+1`;MOD_LT]
THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
;




SUBGOAL_THEN `!t. t< x-i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+ t) + 1)) = &2`
ASSUME_TAC
;


REMOVE_ASSUM_TAC
THEN INDUCT_TAC
;




STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
THEN DICH_TAC(24-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;

STRIP_TAC
THEN MP_TAC(ARITH_RULE`i MOD k< x/\ SUC t< x - i MOD k
==> t< x - i MOD k`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN ABBREV_TAC`j1=i MOD k+t`
THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
THEN MP_TAC SCS_M_LE_K
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`SUC t < x - i MOD k/\ x<k /\ i MOD k<x/\ 3<k==>  i MOD k + t <k /\ ~(i MOD k+t= x)/\ ~((i MOD k +t)+1=x)/\ (i MOD k + t)+1 <k/\ ~(k=0)`)
THEN RESA_TAC;



THAYTHEL_ASM_TAC (41-19)[`j1`][ARITH_RULE` SUC i= i+1`;]
THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
THEN DICH_TAC 1
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[MOD_LT];



MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
THEN RESA_TAC
;


MP_TAC SCS_M_LE_K
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD k <= i MOD k /\ i MOD k< x /\ x<k
==> (i MOD k- j MOD k) < i MOD k + k - x /\ i MOD k + k - (i MOD k - j MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
THEN RESA_TAC
THEN THAYTHE_TAC 6[`i MOD k - j MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+j MOD k`;`v:num->real^3`;`(1*k+j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(j MOD k)`;`v:num->real^3`;`(1*k+ SUC(j MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;




STRIP_TAC
THEN MP_TAC(ARITH_RULE`~(j MOD k= x)==> j MOD k< x \/ x< j MOD k`)
THEN RESA_TAC
;


MP_TAC(ARITH_RULE`j MOD k< x/\ i MOD k<= j MOD k==> j MOD k- i MOD k< x- i MOD k /\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
THEN RESA_TAC
THEN THAYTHE_TAC (30-25)[`j MOD k- i MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
;



MP_TAC(ARITH_RULE`i MOD k< x/\ x< j MOD k /\ j MOD k<k==> i MOD k+k- j MOD k< i MOD k+ k- x
/\ i MOD k +k -(i MOD k+k- j MOD k)= j MOD k`)
THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;DIVISION]
THEN RESA_TAC
THEN THAYTHE_TAC (30-24)[`i MOD k+k- j MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
;






SUBGOAL_THEN `!t. t< x +k- i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+t) + 1)) = &2`
ASSUME_TAC
;



INDUCT_TAC
;




STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
THEN DICH_TAC(24-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;

STRIP_TAC
THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t< x +k- i MOD k
==> t< x +k - i MOD k`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN ABBREV_TAC`j1=i MOD k+t`
THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
THEN MP_TAC SCS_M_LE_K
THEN RESA_TAC
THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;

MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
THEN RESA_TAC
;




MP_TAC(ARITH_RULE`x<i MOD k ==> ~(i MOD k +t =x) `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];


MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= i MOD k +t ==>  (i MOD k+t) -k<k/\ ~((i MOD k+t) -k= x)/\ i MOD k+t = 1*k+ (i MOD k+t) -k`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];





SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;

MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
THEN RESA_TAC
;


MP_TAC(ARITH_RULE`x<i MOD k ==> ~((i MOD k +t) +1=x) `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];


MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= (i MOD k +t)+1 ==>  ((i MOD k+t)+1) -k<k/\ ~(((i MOD k+t) +1)-k= x)/\ (i MOD k+t)+1 = 1*k+ ((i MOD k+t) +1)-k`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];


THAYTHEL_ASM_TAC (38-19)[`j1`][ADD1]
THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`]
;





SUBGOAL_THEN `!t. t< i MOD k- x ==> dist ((v:num->real^3) (i MOD k-t),v ( (i MOD k-t) + 1)) = &2`
ASSUME_TAC
;


REMOVE_ASSUM_TAC
THEN INDUCT_TAC
;


STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE`a-0=a`;GSYM ADD1]
THEN DICH_TAC(24-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;

STRIP_TAC
THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t<  i MOD k-x
==> t<  i MOD k- x`)
THEN RESA_TAC
THEN DICH_TAC 2
THEN RESA_TAC
THEN ABBREV_TAC`j1=i MOD k-(t+1)`
THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
THEN RESA_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
THEN DICH_TAC(35-24)
THEN MP_TAC(ARITH_RULE`SUC t< i MOD k- x /\ x< i MOD k/\ i MOD k<k==> i MOD k - t=(i MOD k - (t+1)) + 1/\ i MOD k - t +1=(i MOD k - (t+1)) + 2/\ i MOD k - (t+1)<k/\ (i MOD k - (t+1))+1<k/\ ~((i MOD k - (t+1))+1= x)/\ ~((i MOD k - (t+1))= x)`)
THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC Cqaoqlr.CQAOQLR
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
THEN MATCH_DICH_TAC 0
;



THAYTHEL_ASM_TAC (41-19)[`j1`][ADD1;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
THEN THAYTHES_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
;





STRIP_TAC
THEN MP_TAC(ARITH_RULE`~(j MOD k = x)==> j MOD k< x\/ x< j MOD k`)
THEN RESA_TAC;



MP_TAC(ARITH_RULE`j MOD k< x/\ x< i MOD k/\ i MOD k<k==> j MOD k+ k- i MOD k< x+k- i MOD k/\ i MOD k+(j MOD k+ k- i MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
THEN RESA_TAC
THEN THAYTHE_TAC 6[`j MOD k+ k- i MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + j MOD k`;`v:num->real^3`;`(1 * k + j MOD k)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + SUC(j MOD k)`;`v:num->real^3`;`(1 * k + SUC(j MOD k))MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;` SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
;


MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
THEN RESA_TAC
;


MP_TAC(ARITH_RULE`x< j MOD k/\ j MOD k<= i MOD k==> i MOD k- j MOD k< i MOD k - x/\ i MOD k- (i MOD k- j MOD k)= j MOD k`)
THEN RESA_TAC
THEN THAYTHE_TAC (30-25)[`i MOD k- j MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
;


MP_TAC(ARITH_RULE`i MOD k<= j MOD k /\ j MOD k< k ==> j MOD k- i MOD k< x+k-i MOD k/\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
THEN RESA_TAC
THEN THAYTHE_TAC (30-24)[`j MOD k- i MOD k`]
THEN DICH_TAC 0
THEN DICH_TAC(29-7)
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
;

]);;



 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)