proposition: Lemma on_vert_edge_above_low_right v c p : left_limit c < right_limit c -> closed_cell_side_limit_ok c -> on_vert_edge p v -> v \in cell_safe_exits_right c -> ~~ (p <<= low c).
proof: Proof. move=> llr cok onv vin. have /andP[/andP[vtople xcond] xcond2] := right_vertical_edge_wrt_low llr cok vin. move: (cok); rewrite /closed_cell_side_limit_ok. rewrite 4!andbA=> /andP[] _. move=> /andP[] rightn0 /andP[] samexr /andP[] sortr /andP[] ronl _. rewrite /point_under_edge -ltNge. set l := (p.1 - (left_pt (low c)).1) / ((right_pt (low c)).1 - (left_pt (low c)).1). set q := ((left_pt (low c)).1 + l * ((right_pt (low c)).1 - (left_pt (low c)).1), (left_pt (low c)).1 + l * ((right_pt (low c)).2 - (left_pt (low c)).2)). case pq : p => [p1 p2]. case lq : (left_pt (low c)) => [q1 q2]. case rq : (right_pt (low c)) => [r1 r2]. have lv : l = (p1 - q1) / (r1 - q1) by rewrite /l pq rq lq /=. have q1ltp1 : q1 < p1. move: onv xcond => /andP[] /eqP + _. by rewrite lq rq pq /= => -> => /andP[]. have lgt0 : 0 < l. rewrite /l divr_gt0 // subr_gt0 ?pq ?lq ?rq //=. by move: (edge_cond (low c)); rewrite lq rq. rewrite det_inverse det_cyclique oppr_gt0. rewrite -(pmulr_rlt0 _ lgt0). rewrite detDM1 det_cyclique. have <- : p1 = q1 + l * (r1 - q1). rewrite lv mulfVK; first by ring. rewrite subr_eq0; apply/eqP=> abs. by have := edge_cond (low c); rewrite lq rq abs lt_irreflexive. rewrite detVert lv. rewrite pmulr_llt0; last by rewrite subr_gt0. have proj2: (head dummy_pt (right_pts c)).2 = q2 + (p1 - q1) / (r1 - q1) * (r2 - q2). have ecnd : (left_pt (low c)).1 != (right_pt (low c)).1. by apply/eqP=> abs; have := edge_cond (low c); rewrite abs lt_irreflexive. have := vert_projl (head dummy_pt (right_pts c)) ecnd. move: ronl=> /andP[] _ -> => /esym /eqP; rewrite ?pq ?lq ?rq /= => ->. rewrite -(eqP xcond2); move: onv=>/andP[] /eqP <- _; rewrite pq /=; ring. rewrite -proj2 subr_lt0. apply: (le_lt_trans vtople). by move: onv=> /andP[] _ /andP[]; rewrite pq /=. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection