proposition: Lemma least_is_inf r X a: order r -> sub X (substrate r) -> least_induced r X a -> greatest_lower_bound r X a.
proof: Proof. move=> or Xsr []; rewrite (proj2 (iorder_osr or Xsr)) => aX h. apply/(glbP or Xsr); split. split; [by apply: Xsr | by move=> y yX; move: (h _ yX); apply:iorder_gle1]. by move=> z [zs h2]; apply: (h2 _ aX). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)