proposition: Lemma induced_sub_pr2 r X: order r -> (forall a b, inc a (substrate r) -> inc b (substrate r) -> (gle r a b <-> sub a b)) -> sub X (substrate r) -> inc (union X) (substrate r) -> least_upper_bound r X (union X).
proof: Proof. move=> or rs Xsr Usr. apply /(lubP or Xsr); split. split => // y yx; apply/rs=> // ;[ by apply: Xsr | by apply: setU_s1 ]. move=> z zu; move: (zu)=> [zr zu1]; apply/rs => //. apply: (induced_sub_pr1 (r:=r)) =>// a b ab; rewrite -rs //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)