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




module   Pcrttid= 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;;



let tri_stable=new_definition
`tri_stable k d s a b J f<=> 
constraint_system k d s a b J f /\ k=3
/\ 
(!i j. i IN s /\ j IN s /\ ~(i=j) ==> &2<= a(i,j)) /\
(!i. i IN s==> a(i,i)= &0 /\ b(i,f i)< &4)/\
(!i j.  {i,j} IN J ==> a(i,j)= sqrt(&8) /\ b(i,j) =cstab)`;;
let EAR_TRI_STABLE_SYSTEM=
prove_by_refinement( `tri_stable 3 ((#0.11)) (0..2) (a_ear0 {{1,2}}) (b_ear0 {{1,2}}) ({{1,2}}) (\i. (1 + i) MOD 3)`,
[ MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`2`][ARITH_RULE`(2+1)-0=3`] THEN ASM_SIMP_TAC[tri_stable;constraint_system;torsor;ARITH_RULE`3<= 3 /\3<=6/\ 1+3<=6/\ (2+1)-0=3/\ 3=3`;CARD_NUMSEG;Hypermap.CARD_SINGLETON;] THEN REMOVE_ASSUM_TAC THEN STRIP_TAC; STRIP_TAC; STRIP_TAC; REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`] THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`2`[ARITH_RULE`SUC 2=3`]; STRIP_TAC; REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`] THEN REPEAT STRIP_TAC THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`i:num`] THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`) THEN ASM_REWRITE_TAC[] THEN RESA_TAC THEN ARITH_TAC; REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`] THEN REPEAT STRIP_TAC THEN ASSUME_TAC(ARITH_RULE`1<=3 /\1<3/\ 1<=2`) THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`3:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`x:num`][ARITH_RULE`1*3=3`] THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`) THEN ASM_REWRITE_TAC[] THEN RESA_TAC THEN ARITH_TAC; STRIP_TAC; REWRITE_TAC[b_ear0;a_ear0] THEN REPEAT GEN_TAC THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =j MOD 3 \/ ~(i MOD 3 =j MOD 3:num)`); ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`]; ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`{i MOD 3,j MOD 3} IN {{1,2}} \/ ~({i MOD 3,j MOD 3} IN {{1,2}})`); ASM_REWRITE_TAC[IN_SING] THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_SING;cstab] THEN RESA_TAC THEN MATCH_MP_TAC REAL_LE_LSQRT THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[IN_SING] THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_SING;h0] THEN RESA_TAC THEN REAL_ARITH_TAC; STRIP_TAC; REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`j:num`][ARITH_RULE`1*3=3`] THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`j:num`;`3:num`] THEN SIMP_TAC[b_ear0;a_ear0;ARITH_RULE`A+0=A`;MOD_MOD_REFL;ARITH_RULE`~(3=0)`]; REWRITE_TAC[SUBSET;IN_SING;IN_ELIM_THM;IN_NUMSEG] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`1` THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`]; STRIP_TAC; REWRITE_TAC[a_ear0;IN_NUMSEG] THEN REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`i<= 2/\ j<= 2==> i< 3 /\ j< 3`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`i:num`;`3`] THEN MRESA_TAC MOD_LT[`j:num`;`3`] THEN DISJ_CASES_TAC(SET_RULE`{i,j} IN {{1,2}} \/ ~({i,j} IN {{1,2}})`); ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RSQRT THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; STRIP_TAC; REWRITE_TAC[b_ear0;a_ear0;MOD_MOD_REFL] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =(1+i) MOD 3 MOD 3\/ ~(i MOD 3 =(1+i) MOD 3 MOD 3:num)`); ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`;cstab] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`{i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}} \/ ~({i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}})`); ASM_REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; REWRITE_TAC[IN_SING;a_ear0;b_ear0] THEN REPEAT STRIP_TAC THEN MP_TAC(SET_RULE`{i,j}={1,2} /\ ~(1=2) ==> ~(i=j) /\ (i =1\/ i=2) /\ (j=1\/ j=2)`) THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=2)`] THEN DISCH_TAC THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`i:num`;`3`] THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;
let exist_tri_stable=
prove_by_refinement(`?s:(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num)). tri_stable (FST s) (FST (SND s)) (FST (SND (SND s))) (FST (SND (SND (SND s)))) (FST(SND (SND (SND (SND s))))) (FST (SND (SND (SND (SND (SND s)))))) (SND(SND (SND (SND (SND (SND s))))))`,
[EXISTS_TAC`3, (#0.11), (0..2), (a_ear0 {{1,2}}), (b_ear0 {{1,2}}), ({{1,2}}),(\i. (1 + i) MOD 3)` THEN REWRITE_TAC[EAR_TRI_STABLE_SYSTEM]]);;
let tri_sy_tybij = (new_type_definition "tri_sy" ("tri_sy", "tuple_tri_sy")exist_tri_stable);;
let k_ts = new_definition `k_ts (s:tri_sy) = FST (tuple_tri_sy s)`;;
let d_ts = new_definition `d_ts (s:tri_sy) = (FST (SND (tuple_tri_sy s)))`;;
let I_TS = new_definition `I_TS (s:tri_sy) = (FST (SND (SND  (tuple_tri_sy s))))`;;
let a_ts = new_definition `a_ts (s:tri_sy) = (FST (SND (SND (SND (tuple_tri_sy s)))))`;;
let b_ts = new_definition `b_ts (s:tri_sy) = (FST(SND (SND (SND (SND (tuple_tri_sy s)))))) `;;
let J_TS = new_definition `J_TS (s:tri_sy) = (FST (SND (SND (SND (SND (SND  (tuple_tri_sy s))))))) `;;
let f_ts = new_definition `f_ts (s:tri_sy) = (SND(SND (SND (SND (SND (SND  (tuple_tri_sy s)))))))`;;
let tri_sy_lemma=
prove(`!s:tri_sy. tri_stable (k_ts s) (d_ts s) (I_TS s) (a_ts s) (b_ts s) (J_TS s) (f_ts s)`,
ASM_REWRITE_TAC[tri_sy_tybij;k_ts;d_ts;I_TS; a_ts; b_ts; J_TS; f_ts]);;
let augmented_constraint_system1=new_definition
`augmented_constraint_system1 (s:stable_sy) I_lo I_str a b m <=>
d_sy s <= # 0.9
/\ m=CARD {i | i IN I_SY s /\ (?j. j IN I_SY s /\( &2< a_sy s (i,j) \/ &2* h0< b_sy s (i,j)))} DIV 2
/\ m+k_sy s <= 6
/\ (!i j. i IN I_SY s /\ j IN I_SY s ==>
a_sy s (i,j)<= a (i,j)
/\ a (i,j)<= b (i,j)
/\ b (i,j)<= b_sy s (i,j))`;;
let augmented_constraint_system2=new_definition
`augmented_constraint_system3 (s:tri_sy) I_lo I_str a b m <=>
d_ts s <= # 0.9
/\ m=CARD {i | i IN I_TS s /\ (?j. j IN I_TS s /\( &2< a_ts s (i,j) \/ &2* h0< b_ts s (i,j)))} DIV 2
/\ m+k_ts s <= 6
/\ (!i j. i IN I_TS s /\ j IN I_TS s ==>
a_ts s (i,j)<= a (i,j)
/\ a (i,j)<= b (i,j)
/\ b (i,j)<= b_ts s (i,j))`;;
let CLOSED_TRI_SY=
prove_by_refinement(` tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> closed {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }`,
[REWRITE_TAC[CONDITION2_SY;CONDITION1_SY;tri_stable] THEN REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN DISCH_THEN(LABEL_TAC"THYGIANG2") THEN DISCH_THEN(LABEL_TAC"THYGIANG") THEN DISCH_THEN(LABEL_TAC"THYGIANG1") THEN REPEAT STRIP_TAC THEN EXISTS_TAC`vecmats (l:real^(M,3)finite_product)` THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SKOLEM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY1") THEN DISCH_THEN(LABEL_TAC"THY2") THEN SUBGOAL_THEN` !i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) ==> ((\n. row i (v n) - row j ((v:num->real^3^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) sequentially`ASSUME_TAC; SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY] THEN REPEAT STRIP_TAC THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`] THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`) THEN RESA_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY2") THEN EXISTS_TAC`N:num` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`) THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^3^M) n) - row i (vecmats (l:real^(M,3)finite_product))`;`--(row j ((v:num->real^3^M) n) - row j (vecmats (l:real^(M,3)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; SUBGOAL_THEN` !i. 1 <= i /\ i <= dimindex (:M) ==> ((\n. row i ((v:num->real^3^M) n)) --> row i (vecmats (l:real^(M,3)finite_product))) sequentially`ASSUME_TAC; SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY] THEN REPEAT STRIP_TAC THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`] THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`) THEN RESA_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY2") THEN EXISTS_TAC`N:num` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`) THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU2") THEN SUBGOAL_THEN`(!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) ==> (a:num#num->real) (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\ norm (row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) <= (b:num#num->real) (i,j))` ASSUME_TAC; REPEAT STRIP_TAC; MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(a:num#num->real)(i,j)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]; MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(b:num#num->real)(i,j)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]; ASM_REWRITE_TAC[] THEN MP_TAC COMPACT_BALL_ANNULUS THEN ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED] THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[ IN_ELIM_THM; dist] THEN REWRITE_TAC[SKOLEM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`(\n. row i ((v:num->real^3^M) n)) `;` row i (vecmats (l:real^(M,3)finite_product))`]) THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[]]);;
let BOUNDED_TRI_SY=
prove(` tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> bounded {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v}`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC`{matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) }` THEN MP_TAC COMPACT_BALL_ANNULUS_MATVEC THEN SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED] THEN RESA_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN SET_TAC[]);;
let COMPACT_TRI_STABLE= 
prove (` tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> compact {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }`,
SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_TRI_SY; CLOSED_TRI_SY;] THEN REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`2<k ==> 1<k`) THEN RESA_TAC THENL[ MRESA_TAC (GEN_ALL BOUNDED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]; MRESA_TAC (GEN_ALL CLOSED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]]);;
let PCRTTID=
prove(`(!d J k a b. tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> compact {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }) /\ (!d J k a b. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> compact {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v /\ CONDITION2_SY v })`,
STRIP_TAC THEN REPEAT GEN_TAC THEN MESON_TAC[COMPACT_TRI_STABLE;WJSCPRO]);;
end;;