proposition: Lemma unlift_some n (h i : 'I_n) : h != i -> {j | i = lift h j & unlift h i = Some j}.
proof: Proof. rewrite eq_sym => /eqP neq_ih. by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)