proposition: Lemma infimum_setU1 a b: sub a E -> has_infimum r a -> inc b E -> infimum r (a +s1 b) = inf r (infimum r a) b.
proof: Proof. move: lr => [or _]; move=> asr hsa bsr; symmetry; apply: infimum_pr2 => //. by apply: lattice_finite_inf1 => //;apply: infimum_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)