proposition: Lemma decomp_swap (n : nat) (s : 'S_n.+2) (K : s ord0 != ord0) : tperm ord0 (s ord0) = ((tperm (lift ord0 ord0) (s ord0)) * (tperm ord0 (lift ord0 ord0)) * (tperm (lift ord0 ord0) (s ord0)))%g :> 'S_n.+2.
proof: Proof. apply /permP => /= i. have [->|Hi] := eqVneq i ord0; first by do ! rewrite permE /=; have -> : (if ord0 == s ord0 then lift ord0 ord0 else ord0) = ord0 by move => n0; rewrite ifN_eqC //=. do ! rewrite permE /=. rewrite ifN_eq //. have [->|Hi1] := eqVneq i (lift ord0 ord0). - have [->|Hs] := eqVneq (s ord0) (lift ord0 ord0); first by by have -> : (if lift ord0 ord0 == ord0 then lift ord0 ord0 else ord0) = ord0. by rewrite (negbTE K) eqxx (negbTE Hs). have [His|His] := eqVneq i (s ord0); first by have -> : (if lift ord0 ord0 == lift ord0 ord0 then ord0 else lift ord0 ord0) = ord0; [by move => *; rewrite eq_refl|rewrite ifN_eqC //|done]. have -> : (if i == ord0 then lift ord0 ord0 else if i == lift ord0 ord0 then ord0 else i) = i by rewrite !ifN_eq. by rewrite !ifN_eq. 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