proposition: Lemma slice_0L s y : &:s (Interval -oo y) = &:s (Interval (BLeft 0%N) y).
proof: Proof. by rewrite /slice /= addn0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)