proposition: Lemma lift_permK i j s : cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).
proof: Proof. rewrite /lift_perm_fun => k. by case: (unliftP i k) => [j'|] ->; rewrite (liftK, unlift_none) ?permK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)