proposition: Lemma shl_itv_add i n m : shl_itv (shl_itv i n) m = shl_itv i (n+m).
proof: Proof. by case: i=>i j /=; rewrite !shl_bnd_add. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)