proposition: Lemma in01_conv (t u v : R) : in01 t -> in01 u -> in01 v -> in01 ((u : R^o) <| t |> v).
proof: Proof. move=>/andP[t0 t1] /andP[u0 u1] /andP[v0 v1]; apply/andP; split. apply addr_ge0; apply mulr_ge0=>//. by rewrite subr_ge0. have<-: t + (1-t) = 1 by rewrite addrCA subrr addr0. apply ler_add; rewrite -subr_ge0. rewrite -{1}[t]mulr1 -mulrBr; apply mulr_ge0=>//. by rewrite subr_ge0. by rewrite -{1}[1-t]mulr1 -mulrBr; apply mulr_ge0; rewrite subr_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise