proposition: Lemma convACA (t u v : R) (a b c d : E) : in01 t -> in01 u -> in01 v -> (a <| u |> b) <| t |> (c <| v |> d) = (a <| t * u / ((u : R^o) <| t |> v) |> c) <| (u : R^o) <| t |> v |> (b <| t * (1 - u) / ((1 - u : R^o) <| t |> (1 - v)) |> d).
proof: Proof. move=>/andP[t0 t1]/andP[u0 u1]/andP[v0 v1]. move:t0; rewrite le0r => /orP[|]. by move=>/eqP->; rewrite !mul0r !conv0. move=>t0; move:t1; rewrite -subr_ge0 le0r => /orP[|]. rewrite subr_eq0=>/eqP<-; rewrite !mul1r !conv1. move:u0; rewrite le0r => /orP[|]. by move=>/eqP->; rewrite subr0 !conv0 divff ?oner_neq0// conv1. rewrite lt0r=>/andP[u0 _]; rewrite divff// conv1. move:u1; rewrite -subr_ge0 le0r => /orP[|]. by rewrite subr_eq0=>/eqP<-; rewrite 2!conv1. by rewrite lt0r=>/andP[t1 _]; rewrite divff// conv1. move=>t1. have c0: forall x y : R, 0 <= x -> 0 <= y -> (x : R^o) <| t |> y = 0 -> x = 0 /\ y = 0. move=>x y; rewrite le0r => /orP[|]. move=>/eqP-> _ /eqP. rewrite/conv scaler0 add0r mulf_eq0 => /orP[|]. by move=>t1'; move:t1; rewrite lt0r=>/andP[/negPf]; rewrite t1'. by move=>/eqP->. move=>x0 y0 c0. suff: 0 < (x : R^o) <| t |> y by rewrite c0 ltxx. rewrite /conv -(addr0 0) ; apply ltr_le_add. by apply mulr_gt0. by apply mulr_ge0=>//; apply ltW. have [|uv0] := eqVneq ((u : R^o) <| t |> v) 0. by move=>/(c0 _ _ u0 v0) [-> ->]; rewrite convmm !conv0 subr0 convmm -mulrA divff ?oner_neq0// mulr1. move:u1 v1; rewrite -2![_ <= 1]subr_ge0=>u1 v1. have [|uv0'] := eqVneq ((1 - u : R^o) <| t |> (1 -v)) 0. by move=> /(c0 _ _ u1 v1)[/eqP]; rewrite subr_eq0=>/eqP<- /eqP; rewrite subr_eq0=>/eqP<-; rewrite convmm !conv1 -mulrA divff ?oner_neq0// mulr1. rewrite{1 2 3 4 6 8}/conv 4!scalerDr 2!addrA !scalerA -conv_onem. rewrite 2![((_ : R^o) <| _ |> _) * (1 - _)]mulrBr 2![_ * (_ * _ / _)]mulrC -!mulrA 2![_^-1 * _]mulrC divff// divff// !mulr1 /conv [t *: _ + _ + _]addrAC subrr add0r [t *: _ + _ + _]addrAC subrr add0r; congr add. by rewrite -2!addrA; congr add; rewrite addrC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise