proposition: Lemma least_of_induced r s x: order r -> sub s (substrate r) -> inc x s -> least r x -> the_least r = the_least_induced r s.
proof: Proof. move=> or ssr xs grx. move: (iorder_osr or ssr) => [pa pb]. rewrite (the_least_pr2 or grx). symmetry; apply: the_least_pr2 => //. hnf; rewrite /the_least_induced pb; split => //. by move => y yxs; apply/iorder_gle0P => //;apply (proj2 grx); apply: ssr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)