proposition: Lemma right_vertical_edge_wrt_low c v : left_limit c < right_limit c -> closed_cell_side_limit_ok c -> v \in cell_safe_exits_right c -> ((head dummy_pt (right_pts c)).2 <= ve_bot v) && ((left_pt (low c)).1 < ve_x v <= (right_pt (low c)).1) && (ve_x v == (head dummy_pt (right_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 vxright : ve_x v = right_limit c. move: vin. rewrite /right_limit /cell_safe_exits_right. elim/last_ind: (right_pts c) rightn0 samexr => [ // | lh e1 Ih] _ /=. elim/last_ind: lh Ih => [ // | lh e2 _] Ih samexr. rewrite last_rcons !rev_rcons/=. rewrite inE=> /orP[/eqP -> /= | vin]. by rewrite (eqP (samexr e1 _)) // mem_rcons inE eqxx. rewrite (eqP (samexr e1 _)); last by rewrite mem_rcons inE eqxx. rewrite -(eqP (samexr e2 _)); last by rewrite !(mem_rcons, inE) eqxx ?orbT. rewrite [e2](_ : _ = last dummy_pt (rcons lh e2)); last by rewrite last_rcons. apply: Ih=> /=. by case lhq: lh. move=> x xin. rewrite (eqP (samexr x _)); last by rewrite mem_rcons inE xin orbT. by rewrite 3!headI /=. rewrite [head _ (rcons _ _)] (_ : _ = head dummy_pt (rcons lh e2)) in vin; last first. by rewrite 3!headI /=. by rewrite rev_rcons; apply: vin. apply/andP; split; last first. rewrite vxright /right_limit; apply: samexr. by case: (right_pts c) rightn0=> [// | ? ?]; rewrite /= mem_last. move: llr. rewrite vxright /right_limit. move: ronl=> /andP[] /andP[] _ + _ /=. rewrite -(eqP (samexr (last dummy_pt (right_pts c)) _)); last first. by case: (right_pts c) rightn0 => [// | ? ?]; rewrite /= mem_last. move=> -> xcond; rewrite ?andbT. rewrite (le_lt_trans _ xcond) ?andbT; last by move: lonl=> /andP[] /andP[]. move: vin; rewrite /cell_safe_exits_right. elim/last_ind: (right_pts c) rightn0 sortr samexr=> [// | + e1 ]. elim/last_ind=> [// | l e2 _] Ih _ sortr samexr. have cmp : e2.2 < e1.2. move: sortr; rewrite -2!cats1 -catA /= map_cat=> /cat_sorted2[_ /=]. by rewrite andbT. have {}sortr : sorted <%R [seq p.2 | p <- rcons l e2]. by move: sortr; rewrite -cats1 map_cat=> /cat_sorted2[]. rewrite [head dummy_pt _](_ : _ = head e2 l); last by rewrite 2!headI /=. rewrite 2!rev_rcons /= inE => /orP[/eqP -> /= | vin]. case lq : l => [// | e3 l'] /=. move: sortr; rewrite lq /= => /(sub_path ltW). rewrite (path_sortedE le_trans)=> /andP[] /allP + _; apply. by apply/mapP; exists e2; rewrite // mem_rcons inE eqxx. rewrite [X in X.2 <= _](_ : _ = head dummy_pt (rcons l e2)); last first. by case lq: l. apply Ih=> //=. by case lq : l. move=> x xin. have -> : head dummy_pt (rcons l e2) = head dummy_pt (rcons (rcons l e2) e1). by case lq : l. by apply: samexr; rewrite mem_rcons inE xin orbT. have -> : head dummy_pt (rcons l e2) = head dummy_pt (rcons (rcons l e2) e1). by case lq : l. by rewrite rev_rcons 2!headI /=. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection