proposition: Lemma OFS_in_fin x y: inc x y -> finite_o y -> finite_o x.
proof: Proof. move=> xy [oy niy]. have ox:=(Os_ordinal oy xy). by split => //; dneg nix; apply: (OIS_in_inf oy xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)