proposition: Lemma least_elementP X r: order r -> sub X (substrate r) -> (has_least (induced_order r X) <-> (exists2 x, lower_bound r X x & inc x X)).
proof: Proof. rewrite /lower_bound/has_least/least=> or Xr. rewrite (proj2 (iorder_osr or Xr)); split. move=> [a [aX h]]; exists a => //;split; first by apply:Xr. move=> y yX; move: (h _ yX); apply:iorder_gle1. move=> [x [xsr hyp] xX]; ex_tac. by move=> y yX; apply/iorder_gle0P => //; apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)