proposition: Lemma OIS_le_inf x y: x <=o y -> infinite_o x -> infinite_o y.
proof: Proof. case/ole_eqVlt; [ by move -> | move => lt]. exact: (OIS_in_inf (proj32_1 lt) (olt_i lt)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)