proposition: Lemma neq_bump h i : h != bump h i.
proof: Proof. rewrite /bump eqn_leq; have [le_hi | lt_ih] := leqP h i. by rewrite ltnNge le_hi andbF. by rewrite leqNgt lt_ih. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)