proposition: Lemma shl_itv0 i : shl_itv i 0%N = i.
proof: Proof. by case: i=>i j /=; rewrite !shl_bnd0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)