proposition: Lemma unbumpKcond h i : bump h (unbump h i) = (i == h) + i.
proof: Proof. rewrite /bump /unbump leqNgt -subSKn. case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn. by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)