proposition: Lemma finite_subset_torder_least r X: total_order r -> finite_set X -> nonempty X -> sub X (substrate r) -> has_least (induced_order r X).
proof: Proof. move=> tor fsX neX Xsr. have or: order r by move: tor=> []. have rtor:=(total_order_opposite tor). move: (opp_osr or) => [aa so]; move: (Xsr); rewrite - so => rXsr. move: (finite_subset_torder_greatest rtor fsX neX rXsr)=> [x []]. rewrite iorder_sr // => xX xg. exists x; hnf;rewrite iorder_sr//;split => //. move=> a aX; move: (iorder_gle1 (xg _ aX)) => /igraph_pP h. by apply /iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)