proposition: Lemma conv_onem (t u v : R) : (1-u : R^o) <| t |> (1-v) = 1 - (u : R^o) <| t |> v.
proof: Proof. rewrite/conv 2!scalerBr addrACA opprD; congr add. have sm: forall u, u *: (1 : R^o) = u*1 by []. by rewrite 2!sm 2!mulr1 addrCA subrr addr0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise