proposition: Lemma lift_permM : forall n i j k s t, (@lift_perm n i j s * lift_perm j k t)%g = lift_perm i k (s * t)%g.
proof: Proof. move=> n i j k s t; apply/permP=> i1; case: (unliftP i i1) => [i2|] ->{i1}. by rewrite !(permM, lift_perm_lift). by rewrite permM !lift_perm_id. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms