proposition: Lemma OIS_in_inf x y: ordinalp y -> inc x y -> infinite_o x -> infinite_o y.
proof: Proof. move => oy xy. move: (ordinal_irreflexive (Os_ordinal oy xy)) => ha. move:(ordinal_irreflexive oy) (ordinal_transitive oy xy) => hb hc [f xx]. have xi: x \Eq (osucc x) by exists f. exact (sub_inf_aux ha hb hc xi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)