proposition: Lemma proj0_inj n (s : 'S_n.+2) : s ord0 = ord0 -> injective (proj0 s).
proof: Proof. move=> s00 i j; rewrite /proj0 => ij. suff : s (lift ord0 i) = s (lift ord0 j) by move/(@perm_inj _ s)/lift_inj. apply val_inj => /=. rewrite -[LHS]prednK ?lt0n; last first. suff : s (lift ord0 i) != ord0 by []. rewrite -[X in _ != X]s00. by apply/eqP => /(@perm_inj _ s). rewrite -[RHS]prednK ?lt0n; last first. suff : s (lift ord0 j) != ord0 by []. rewrite -[X in _ != X]s00. by apply/eqP => /(@perm_inj _ s). move/(congr1 val) : ij => /= ij. rewrite inordK // in ij; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. suff : s (lift ord0 i) != ord0 by []. rewrite -[X in _ != X]s00. by apply/eqP => /(@perm_inj _ s). rewrite inordK // in ij; last first. rewrite prednK ?lt0n; first by rewrite -ltnS. suff : s (lift ord0 j) != ord0 by []. rewrite -[X in _ != X]s00. by apply/eqP => /(@perm_inj _ s). by rewrite ij. 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