proposition: Lemma isOE_le n t : t < n.+1 -> isO n.+1 t = [set inord i | i : 'I_t].
proof: Proof. move=> tLn; apply/setP=> i; rewrite !inE. apply/idP/imsetP => [iLt| [j _ ->]]. by exists (Ordinal iLt); rewrite //=; apply/val_eqP; rewrite /= inordK. by rewrite inordK // (leq_trans _ tLn) // ltnS // ltnW. Qed.
imports: mathcomp(all_ssreflect finmap)