proposition: Lemma slice_size s (i : interval nat) : size (&:s i) = minn (bnd i.2 (size s)) (size s) - bnd i.1 (size s).
proof: Proof. rewrite /slice; case: i=>[[l i|[]][r j|[]]] //=; rewrite ?take0 ?drop0 ?take_size ?drop_size ?minnn ?min0n ?subn0 //=. - by rewrite size_drop size_take_min. - by rewrite size_drop. - by rewrite size_take_min. - by rewrite size_drop size_take_min. by rewrite subnn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)