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