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