proposition: Lemma leq_bump h i j : (i <= bump h j) = (unbump h i <= j).
proof: Proof. rewrite /bump leq_subLR. case: (leqP i h) (leqP h j) => [le_i_h | lt_h_i] [le_h_j | lt_j_h] //. by rewrite leqW (leq_trans le_i_h). by rewrite !(leqNgt i) ltnW (leq_trans _ lt_h_i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)