proposition: Lemma convA t u a b c : in01 t -> in01 u -> a <| t |> (b <| u |> c) = (a <| t / ((1 : R^o) <| t |> u) |> b) <| (1 : R^o) <| t |> u |> c.
proof: Proof. move=> t01 u01. have -> : (1 : R^o) <| t |> u = 1 - (1 - t) * (1 - u). by rewrite (convlr _ (1 : R^o)) -[u-1]opprB scalerN. rewrite/conv scalerDr addrA 2!scalerA opprB addrCA subrr addr0; congr add. have [/eqP|tu1] := eqVneq (1 - (1 - t) * (1 - u)) 0. rewrite {1}subr_eq0 eq_sym in01M1 -?in01_onem// -2![_-_ == 1]subr_eq0. rewrite 2![1-_-1]addrAC subrr 2!add0r 2!oppr_eq0=>/andP[/eqP-> /eqP->]. by rewrite mulr0 subr0 mulr1 subrr 3!scale0r addr0. rewrite scalerDr 2!scalerA [(1-_*_)*(1-_)]mulrBr mulrCA divff// 2!mulr1 mulrBr. by rewrite mulr1 addrAC opprB addrCA subrr addr0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise