proposition: Lemma bumpK h : cancel (bump h) (unbump h).
proof: Proof. rewrite /bump /unbump => i. have [le_hi | lt_ih] := leqP h i; first by rewrite ltnS le_hi subn1. by rewrite ltnNge ltnW ?subn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)