proposition: Lemma lift_perm1 : forall n i, @lift_perm n i i 1 = 1%g.
proof: Proof. by move=> n i; apply: (mulgI (lift_perm i i 1)); rewrite lift_permM !mulg1. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms