proposition: Lemma sup_setU1 X a: sub X E -> nonempty X -> finite_set X -> inc a E -> supremum r (X +s1 a) = sup r (supremum r X) a.
proof: Proof. move => pb pc pd pe; apply:supremum_setU1 => //. by apply: lattice_finite_sup2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)