proposition: Lemma face_trans (A : set E) (F : set E) (G : set E) : face A F -> face F G -> face A G.
proof: Proof. move=>[AF Fconv Fface] [FG Gconv Gface]. split => //. - by move=> x Gx; apply AF, FG. - move=>// x u v xG uA vA xuv xu xv. have [uF vF]: (u \in F /\ v \in F). apply (Fface x)=>//. by apply mem_set, FG, set_mem. by apply (Gface x). Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals