proposition: Lemma s2fD_isO n (s : {set 'I_n}) t : s2f (s :\: isO n t) = s2f s `\` sint 0 t.
proof: Proof. apply/fsetP => j; rewrite !inE. apply/imfsetP/andP => /= [[k]|[jDi /imfsetP[/= k kIs jEk]]]. by rewrite !inE -!mem_s2f mem_sint /= => /andP[kDi kIs] ->. move: jDi; rewrite mem_sint /= -leqNgt => jDi. by exists k; rewrite // !inE -leqNgt kIs -jEk jDi. Qed.
imports: mathcomp(all_ssreflect finmap)