proposition: Lemma conv_num_ltr (a b t c : R) : 0 < t < 1 -> a < c -> b <= c -> (a : R^o) <| t |> b < c.
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 * (c - a)) + (1 - t) * (c - b))); last by ring. have fact1 : 0 < t * (c - a) by apply: mulr_gt0; lra. have fact2 : 0 <= (1 - t) * (c - b) 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