proposition: Lemma sint_sub a b c : a <= c -> [fset i in (sint a b) | c <= i] = sint c b.
proof: Proof. move=> aLc. apply/fsetP => i. rewrite mem_sint. apply/imfsetP/idP => [[j /=]|/andP[cLi iLb]]. rewrite inE mem_sint => /andP[/andP[aLj jLb] cLj] ->. by rewrite cLj. by exists i; rewrite //= inE mem_sint cLi iLb (leq_trans aLc). Qed.
imports: mathcomp(all_ssreflect finmap)