proposition: Lemma on_vert_edge_above_low_left 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_left c -> ~~ (p <<= low c).
proof: Proof. move=> llr cok onv vin. have /andP[/andP[vtople xcond] xcond2] := left_vertical_edge_wrt_low llr cok vin. move: (cok)=> /andP[] leftn0 /andP[] samexl /andP[] sortl. move=>/andP[] _ /andP[] lonl _. rewrite /point_under_edge -ltNge. set l := ((right_pt (low c)).1 - p.1) / ((right_pt (low c)).1 - (left_pt (low c)).1). set q := ((right_pt (low c)).1 - l * ((right_pt (low c)).1 - (left_pt (low c)).1), (right_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 = (r1 - p1) / (r1 - q1) by rewrite /l pq rq lq /=. have p1ltr1 : p1 < r1. 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_cyclique. rewrite -(pmulr_rgt0 _ lgt0). rewrite detDM1 det_cyclique. have <- : p1 = r1 + l * (q1 - r1). rewrite lv -(opprB r1 q1) mulrN 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 nmulr_lgt0; last by rewrite subr_lt0. have proj2: (last dummy_pt (left_pts c)).2 = r2 + (r1 - p1) / (r1 - q1) * (q2 - r2). 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_projr (last dummy_pt (left_pts c)) ecnd. move: lonl=> /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