proposition: Lemma shl_bnd_add i n m : shl_bnd (shl_bnd i n) m = shl_bnd i (n+m).
proof: Proof. case: i=>[[] i|[]] //=. - case: ltnP=>Hin /=; first by rewrite ltn_addr. by rewrite ltn_subLR // subnDA. case: ltnP=>Hin /=; first by rewrite ltn_addr. by rewrite ltn_subLR // subnDA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)