proposition: Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}.
proof: Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)