proposition: Lemma swap_asaE n (s : 'S_n.+2) (K : s ord0 != ord0) : s = (lift_perm ord0 ord0 (PermDef.perm (swap_asa_inj K)) * tperm (ord0) (s ord0))%g.
proof: Proof. apply/permP => i. rewrite [in RHS]permE /=. have [->|i0] := eqVneq i ord0; first by rewrite lift_perm_id permE. have Hi : i = lift ord0 (inord i.-1). apply/val_inj => /=. rewrite /bump leq0n /= add1n inordK. by rewrite prednK // lt0n. by rewrite -ltnS prednK // lt0n. rewrite {2}Hi lift_perm_lift 2!permE /= /swap_asa. case: ifPn => /=. case: ifPn => /=. rewrite inordK; last by rewrite -ltnS prednK // lt0n. rewrite prednK // ?lt0n //. move=> si _. apply: (@perm_inj _ s^-1%g). rewrite permK; exact/eqP. rewrite inordK; last by rewrite -ltnS prednK // lt0n. rewrite prednK // ?lt0n // => si. move/eqP. move/(congr1 (s^-1%g)). rewrite permK => si0. exfalso. move/eqP : i0; apply. rewrite -si0 /=. apply: (@perm_inj _ s). rewrite permKV /=. apply/val_inj => /=. rewrite /bump leq0n add1n. rewrite inordK; last first. rewrite -ltnS prednK // lt0n -Hi. apply: contra si => /eqP si0'. apply/eqP. suff : i = (s^-1)%g ord0 by move/(congr1 val). apply: (@perm_inj _ s). rewrite permKV. exact/val_inj. rewrite prednK //; last first. rewrite lt0n -Hi. apply: contra si => /eqP si0'. apply/eqP. suff : i = (s^-1)%g ord0 by move/(congr1 val). apply: (@perm_inj _ s). rewrite permKV. exact/val_inj. by rewrite -Hi. case: ifPn. rewrite inordK; last by rewrite -ltnS prednK // lt0n. rewrite prednK ?lt0n // => si. move=> L. exfalso. move/eqP : L; apply. apply/val_inj => /=. rewrite /bump leq0n add1n inordK; last by rewrite -ltnS // prednK // lt0n. by rewrite prednK // lt0n. move=> L1 L2. apply/val_inj => /=. rewrite /bump leq0n add1n inordK; last first. rewrite -ltnS prednK // lt0n. apply: contra L1. move/eqP => L1. apply/eqP. rewrite inordK; last by rewrite -ltnS prednK // lt0n. rewrite prednK // ?lt0n //. move: L1. rewrite (_ : lift _ _ = i); last first. apply/val_inj => /=. by rewrite /bump leq0n add1n inordK // ?prednK // ?lt0n // -ltnS. move=> si. have : s i = ord0 by apply/val_inj. move/(congr1 s^-1%g). by rewrite permK => ->. rewrite prednK // ?lt0n; last first. apply: contra L1 => /eqP L1. have {}L1 : s (lift ord0 (inord i.-1)) = ord0 by exact/val_inj. rewrite -L1 permK. exact/eqP. by rewrite -Hi. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex