proposition: Lemma left_vertical_edge_wrt_high c v : left_limit c < right_limit c -> closed_cell_side_limit_ok c -> v \in cell_safe_exits_left c -> (ve_top v <= (head dummy_pt (left_pts c)).2) && ((left_pt (high c)).1 <= ve_x v < (right_pt (high c)).1) && (ve_x v == (head 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 first. rewrite vxleft /left_limit (samexl (last dummy_pt (left_pts c))) //. by case: (left_pts c) leftn0=> [// | ? ?]; rewrite /= mem_last. move: llr. rewrite vxleft /left_limit -(samexl (last dummy_pt (left_pts c))); last first. by case: (left_pts c) leftn0 => //= a tl _ ; rewrite mem_last. move: lonh=> /andP[] /andP[] -> /= _ _ llr. rewrite (lt_le_trans llr) ?andbT; last first. by rewrite /right_limit; move: ronh=> /andP[] /andP[] _ ->. 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 ]. apply: (le_trans _ (ltW cmp)). 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