proposition: Lemma unbumpDl h i k : unbump (k + h) (k + i) = k + unbump h i.
proof: Proof. apply: (can_inj (bumpK (k + h))). by rewrite bumpDl !unbumpKcond eqn_add2l addnCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)