proposition: Lemma conv_num_sg s (a b t : R) : 0 < t < 1 -> sgz a = s -> sgz b = s -> sgz ((a : R^o) <| t |> b) = s.
proof: Proof. move=> tint. have [ -> <- | agt0 <- | alt0 <-] := sgzP a. have [ -> | // | // ] := sgzP b. by rewrite convmm sgz0. have [ // | bgt0 _ | // ] := sgzP b. rewrite /conv; apply/gtr0_sgz/addr_gt0; apply/mulr_gt0; lra. have [ // | // | blt0 _] := sgzP b. rewrite /conv; apply/ltr0_sgz; rewrite -oppr_gt0 opprD. apply/addr_gt0; rewrite -mulrN; apply/mulr_gt0; lra. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection