proposition: Lemma card_sint a b : #|`sint a b| = (b - a).
proof: Proof. elim: b => [|b IH]. apply/eqP; rewrite cardfs_eq0; apply/eqP/fsetP=> i. by rewrite mem_sint andbF inE. have [aLb|bLa] := leqP a b; last first. rewrite (_ : _ - _ = 0); last first. by apply/eqP; rewrite subn_eq0. apply/eqP; rewrite cardfs_eq0; apply/eqP/fsetP=> i; rewrite mem_sint inE ltnS. by apply/idP => /andP[H1 /(leq_trans H1)]; rewrite leqNgt bLa. rewrite (cardfsD1 b) (_ : _ \in _); last by rewrite mem_sint aLb /=. by rewrite sintSr IH subSn. Qed.
imports: mathcomp(all_ssreflect finmap)