proposition: Lemma swap_asa_inj n (s : 'S_n.+2) (K : s ord0 != ord0) : injective (swap_asa s ord0).
proof: Proof. move=> i j; rewrite /swap_asa. case: ifPn => [/eqP Hi|Hi]. case: ifPn => [/eqP Hj ?|Hj]. move: Hi; rewrite -Hj => -[?]; exact/val_inj. move/(congr1 val) => /=. rewrite inordK //; last by rewrite prednK ?lt0n // -ltnS. rewrite inordK; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. suff : s (lift ord0 j) != ord0 by []. by apply: contra Hj => /eqP <-; rewrite permK. move/(congr1 S). rewrite prednK ?lt0n // prednK ?lt0n; last first. apply: contra Hj => Hj. suff : s (lift ord0 j) = ord0 by move=> <-; rewrite permK. exact/eqP. move=> H. suff : s ord0 = s (lift ord0 j) by move/(@perm_inj _ s). exact/val_inj. case: ifPn => Hj. move/(congr1 val) => /=. rewrite inordK; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. apply: contra Hi => Hi. suff : s (lift ord0 i) == ord0 :> 'I_n.+2 by move=> /eqP <-; rewrite permK. by []. rewrite inordK; last by rewrite prednK ?lt0n // -ltnS. move/(congr1 S). rewrite prednK ?lt0n; last first. apply: contra Hi => Hi. suff : s (lift ord0 i) == ord0 :> 'I_n.+2 by move/eqP <-; rewrite permK. by []. rewrite prednK ?lt0n //. move=> Hs. have {Hs} : s (lift ord0 i) = s ord0 by apply/val_inj. by move/(@perm_inj _ s). move/(congr1 val) => /=. move/(congr1 S). rewrite inordK; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. apply: contra Hi => Hi. suff : s (lift ord0 i) == ord0 :> 'I_n.+2 by move/eqP => <-; rewrite permK. by []. rewrite inordK; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. apply: contra Hj => Hj. suff : s (lift ord0 j) == ord0 :> 'I_n.+2 by move/eqP => <-; rewrite permK. by []. rewrite prednK ?lt0n //; last first. apply: contra Hi => Hi. suff : s (lift ord0 i) == ord0 :> 'I_n.+2 by move/eqP => <-; rewrite permK. by []. rewrite prednK ?lt0n; last first. apply: contra Hj => Hj. suff : s (lift ord0 j) == ord0 :> 'I_n.+2 by move/eqP => <-; rewrite permK. by []. move=> Hs. have {Hs} : s (lift ord0 i) = s (lift ord0 j) by exact/val_inj. by move /(@perm_inj _ s)/lift_inj. 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