proposition: Lemma left_vertical_edge_wrt_low c v : left_limit c < right_limit c -> closed_cell_side_limit_ok c -> v \in cell_safe_exits_left c -> ((last dummy_pt (left_pts c)).2 <= ve_bot v) && ((left_pt (low c)).1 <= ve_x v < (right_pt (low c)).1) && (ve_x v == (last dummy_pt (left_pts c)).1).
proof: Proof. move=> llr /andP[] leftn0 /andP[] /allP samexl /andP[] sortl. move=>/andP[] lonh /andP[] lonl. move=> /andP[] rightn0 /andP[] /allP samexr /andP[] sortr /andP[] ronl ronh vin. have {}samexl: {in left_pts c, forall p, (head dummy_pt (left_pts c)).1 = p.1 }. move=> x xin; rewrite (eqP (samexl x xin)). rewrite -(eqP (samexl (head dummy_pt (left_pts c)) _)) //. by move: leftn0; case (left_pts c)=> //= s l _; rewrite inE eqxx. have vxleft : ve_x v = left_limit c. move: vin. rewrite /left_limit /cell_safe_exits_left. elim: (left_pts c) leftn0 samexl => [ // | e1 [// | e2 tl] Ih] _ /= samexl. rewrite inE=> /orP[/eqP -> /= | vin]. by apply: samexl; rewrite inE mem_last orbT. apply: (Ih isT)=> /=. move=> x xin. rewrite -(samexl e2); last by rewrite !inE eqxx orbT. by apply: samexl; rewrite inE xin orbT. by rewrite -(samexl e2) //; rewrite !inE eqxx orbT. apply/andP; split; last by rewrite vxleft. move: llr. rewrite vxleft /left_limit. move: lonl=> /andP[] /andP[] -> /= _ _ llr. rewrite (lt_le_trans llr) ?andbT; last first. rewrite /right_limit; move: ronl=> /andP[] /andP[] _ + _. rewrite -(eqP (samexr (last dummy_pt (right_pts c)) _)) //. by move: rightn0; case: (right_pts c)=> [// | ? ?]; rewrite /= mem_last. move: vin; rewrite /cell_safe_exits_left. elim: (left_pts c) leftn0 sortl samexl => [// | e1 [ // | e2 tl] /(_ isT) Ih] _ /= /andP[] cmp s samexl. rewrite inE=> /orP[/eqP -> /= | vin ]. have sgt : subrel >%R (>=%R : rel R) by move=> x y /ltW. have s' : path >=%R e2.2 [seq p.2 | p <- tl]. by apply: (sub_path sgt). case tlq : tl => [// | e3 tl']; rewrite -tlq. move: s'; rewrite path_sortedE; last by apply/rev_trans/le_trans. move=> /andP[] /allP /(_ (last e2 tl).2) + _; apply. by apply/mapP; exists (last e2 tl); rewrite // tlq /= mem_last. apply Ih=> //=. move=> x xin. by rewrite -(samexl e2) ?inE ?eqxx ?orbT // (samexl x) // inE xin orbT. by rewrite -(samexl e2) // !inE eqxx orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection