proposition: Lemma isOE n t : t <= n -> s2f (isO n t) = sint 0 t.
proof: Proof. move=> tLn. apply/fsetP => i; rewrite mem_sint. apply/imfsetP/idP => /= [[j]|iLt]; first by rewrite inE => jLt ->. have iLn : i < n by apply: leq_trans tLn. by exists (Ordinal iLn); rewrite // inE. Qed.
imports: mathcomp(all_ssreflect finmap)