proposition: Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h).
proof: Proof. by move=> i; case: (unlift_some (neq_lift h i)) => j /lift_inj->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)