proposition: Lemma unlift_subproof n (h : 'I_n) (u : {j | j != h}) : unbump h (val u) < n.-1.
proof: Proof. case: n h u => [|n h] [] //= j ne_jh. rewrite -(leq_bump2 h.+1) bumpS unbumpK // /bump. case: (ltngtP n h) => [|_|eq_nh]; rewrite ?(leqNgt _ h) ?ltn_ord //. by rewrite ltn_neqAle [j <= _](valP j) {2}eq_nh andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)