proposition: Lemma suff_generators0 n (P : 'S_n.+2 -> Prop) : (forall s s', P s -> P s' -> P (s' * s)%g) -> (forall s : 'S_n.+2, P (tperm ord0 (s ord0))) -> (forall s : 'S_n.+2, s ord0 = ord0 -> P s) -> forall s : 'S_n.+2, P s.
proof: Proof. move=> H0 H1 H2 s. have [K|K] := eqVneq (s ord0) ord0; first exact: H2. rewrite (swap_asaE K); apply H0; first exact/H1. by apply H2; rewrite lift_perm_id. 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