proposition: Lemma lattice_finite_sup1 X x a: sub X E -> least_upper_bound r X x -> inc a E -> least_upper_bound r (X +s1 a) (sup r x a).
proof: Proof. move=> Xsr lub asr. have or: (order r) by move: lr => [ok _]. have st: (sub (X +s1 a) (substrate r)) by apply: setU1_sub. move /(lubP or Xsr): lub => [[lu1 lu2] lu3]. have [p1 p2 p3] := (lattice_sup_pr lr lu1 asr). apply /(lubP or st); split. split; first by order_tac. move=> y; case /setU1_P => h;[move: (lu2 _ h)=> h'; order_tac| ue]. move=>z [z1 z2]; apply:p3;[apply: lu3; split => //t tx |];apply: z2; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)