proposition: Lemma generators (s : 'S_2) : s = 1%g \/ s = tperm ord0 (Ordinal (erefl (1 < 2))).
proof: Proof. pose s0 := s ord0. pose s1 := s (Ordinal (erefl (1 < 2))). case/orP : (ord2 s0) => /eqP Hs0. - case/orP : (ord2 s1) => [/eqP |/eqP ?]. + by rewrite -Hs0 => /perm_inj /(congr1 val). + left; apply/permP => i. by case/orP: (ord2 i) => /eqP ->; rewrite perm1. - case/orP : (ord2 s1) => [/eqP ? |/eqP]. + right; apply/permP => i. by case/orP: (ord2 i) => /eqP ->; rewrite permE. + by rewrite -Hs0 => /perm_inj /(congr1 val). 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