proposition: Lemma bumpC h1 h2 i : bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i).
proof: Proof. rewrite {1 5}/bump -leq_bump addnCA; congr (_ + (_ + _)). rewrite 2!leq_bump /unbump /bump; case: (leqP h1 h2) => [le_h12 | lt_h21]. by rewrite subn0 ltnS le_h12 subn1. by rewrite subn1 (ltn_predK lt_h21) (leqNgt h1) lt_h21 subn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)