proposition: Lemma slice_FR s x : &:s (Interval x +oo) = &:s (Interval x (BLeft (size s))).
proof: Proof. by rewrite /slice /= addn0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)