proposition: Lemma convA' t u a b c : in01 t -> in01 u -> (a <| u |> b) <| t |> c = a <| t * u |> (b <| t * (1 - u) / ((1 - u : R^o) <| t |> 1) |> c).
proof: Proof. move=>t01 u01. rewrite convC (convC u) convA. 2, 3: by rewrite -in01_onem. rewrite -convC convC (convC _ c). have -> : (1 - u : R^o) <| t |> 1 = 1 - t * u. by rewrite (convrl _ _ 1) addrAC subrr add0r scalerN. rewrite opprB addrCA subrr addr0. have [/eqP|tu1] := eqVneq (1 - t * u) 0. by rewrite subr_eq0 eq_sym in01M1// =>/andP[/eqP-> /eqP->]; rewrite 2!mul1r 2!conv1. congr (_ <| _ |> (_ <| _ |> _)). by apply (mulfI tu1); rewrite mulrBr mulr1 2![(1-t*u)*(_/_)]mulrCA divff// 2!mulr1 opprB addrCA addrAC subrr add0r mulrBr mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise