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