proposition: Lemma under_proj e p : valid_edge e p -> (p <<= e) = (p.2 <= (left_pt e).2 + (p.1 - (left_pt e).1) * ((right_pt e).2 - (left_pt e).2) / ((right_pt e).1 - (left_pt e).1)).
proof: Proof. move=> vep. rewrite /point_under_edge det_cyclique. have ecnd := edge_cond e. have ecnd' : (left_pt e).1 != (right_pt e).1 by lra. set p' := (p.1, (left_pt e).2 + (p.1 - (left_pt e).1) / ((right_pt e).1 - (left_pt e).1) * ((right_pt e).2 - (left_pt e).2)). have := diff_vert_y ecnd'=> /(_ p p' erefl) /eqP. rewrite subr_eq=> /eqP ->; rewrite /p' /=. rewrite addrA (addrC _ (left_pt e).2) -!addrA. rewrite ler_add2. rewrite addrC -ler_subr_addl mulrAC addrN. rewrite pmulr_lle0 // invr_gt0; lra. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection