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