proposition: Lemma conv_num_gtl (a b t c : R) : 0 < t < 1 -> c < a -> c <= b -> c < (a : R^o) <| t |> b.
proof: Proof. move=> tint clta cleb; rewrite /conv. rewrite -[_ *: (a : R^o)]/(t * a). rewrite -[_ *: (b : R^o)]/((1 - t) * b). rewrite [X in _ < X] (_ : _ = c + ((t * (a - c)) + (1 - t) * (b - c))); last by ring. have fact1 : 0 < t * (a - c) by apply: mulr_gt0; lra. have fact2 : 0 <= (1 - t) * (b - c) by apply: mulr_ge0; lra. lra. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection