proposition: Lemma lift_permM i j k s t : lift_perm i j s * lift_perm j k t = lift_perm i k (s * t).
proof: Proof. apply/permP=> i1; case: (unliftP i i1) => [i2|] ->{i1}. by rewrite !(permM, lift_perm_lift). by rewrite permM !lift_perm_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)