proposition: Theorem sup_increasing r A B: order r -> sub A (substrate r) -> sub B (substrate r) -> sub A B -> has_supremum r A -> has_supremum r B-> gle r (supremum r A) (supremum r B).
proof: Proof. move=> or As Bs AB sA sB. move /(lubP or As): (supremum_pr1 or sA) => [_ p1]. move /(lubP or Bs): (supremum_pr1 or sB) => [[uB p2] _]. by apply: p1; split => // t tA; apply:p2; apply: AB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)