proposition: Lemma add_affine (E : lmodType R_ringType) : affine (fun p : E * E => p.1 + p.2).
proof: Proof. move=>p/= [x0 x1] [y0 y1]/=. by rewrite/conv/= addrACA -2!scalerDr. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals