proposition: Lemma inf_sumE (A B : set R) : has_inf A -> has_inf B -> inf [set x + y | x in A & y in B] = inf A + inf B.
proof: Proof. move/has_inf_supN => ? /has_inf_supN ?; rewrite /inf. rewrite [X in - sup X = _](_ : _ = [set x + y | x in [set - x | x in A ] & y in [set - x | x in B]]). rewrite eqEsubset; split => /= t [] /= x []a Aa. case => b Bb <- <-; exists (- a); first by exists a. by exists (- b); [exists b|rewrite opprD]. move=> <- [y] [b Bb] <- <-; exists (a + b); last by rewrite opprD. by exists a => //; exists b. by rewrite sup_sumE // -opprD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid