proposition: Lemma lift_perm_lift : forall n i j s k, lift_perm i j s (lift i k) = lift j (s k) :> 'I_n.+1.
proof: Proof. by move=> n i j s k; rewrite permE /lift_perm_fun liftK. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms