proposition: Lemma suff_generators (P : 'S_3 -> Prop) : P 1%g -> P p01 -> P p02 -> (forall s s', P s -> P s' -> P (s' * s)%g) -> forall s : 'S_3, P s.
proof: Proof. move=> H1 H2 H3 H s. have : s = 1%g \/ s = S3.p01 \/ s = S3.p02 \/ s = S3.p12 \/ s = S3.p021 \/ s = S3.p012. pose s0 := s ord0. pose s1 := s (Ordinal (erefl (1 < 3))). pose s2 := s (Ordinal (erefl (2 < 3))). case/or3P : (ord3 s0) => [/eqP Hs0|/eqP Hs0|/eqP Hs0]. - case/or3P : (ord3 s1) => [/eqP|/eqP Hs1|/eqP Hs1]. + by rewrite -Hs0 => /perm_inj. + case/or3P : (ord3 s2) => [/eqP|/eqP Hs2|/eqP]. * by rewrite -Hs0 => /perm_inj. * by move: Hs1; rewrite -Hs2 => /perm_inj. * left. apply/permP => /= i. case/or3P : (ord3 i) => /eqP ->; by rewrite permE //. + case/or3P : (ord3 s2) => [/eqP|/eqP Hs2|/eqP]. * by rewrite -Hs0 => /perm_inj. * right; right; right; left. apply/permP => /= i. by case/or3P : (ord3 i) => /eqP ->; rewrite permE. * by rewrite -Hs1 => /perm_inj. - case/or3P : (ord3 s1) => [/eqP Hs1|/eqP|/eqP Hs1]. + case/or3P : (ord3 s2) => [/eqP|/eqP|/eqP Hs2]. * by rewrite -Hs1 => /perm_inj. * by rewrite -Hs0 => /perm_inj. * right; left. apply/permP => /= i. by case/or3P : (ord3 i) => /eqP ->; rewrite permE. + by rewrite -Hs0 => /perm_inj. + case/or3P : (ord3 s2) => [/eqP Hs2|/eqP|/eqP]. * right; right; right; right; left. apply/permP => /= i. by case/or3P : (ord3 i) => /eqP ->; rewrite !permE //= !permE. * by rewrite -Hs0 => /perm_inj. * by rewrite -Hs1 => /perm_inj. - case/or3P : (ord3 s1) => [/eqP Hs1|/eqP Hs1|/eqP Hs1]. + case/or3P : (ord3 s2) => [/eqP Hs2|/eqP Hs2|/eqP Hs2]. * by move: Hs1; rewrite -Hs2 => /perm_inj. * right; right; right; right; right. apply/permP => /= i. by case/or3P : (ord3 i) => /eqP ->; rewrite !permE //= !permE. * by move: Hs0; rewrite -Hs2 => /perm_inj. + case/or3P : (ord3 s2) => [/eqP Hs2|/eqP Hs2|/eqP Hs2]. * right; right; left. apply/permP => /= i. by case/or3P : (ord3 i) => /eqP ->; rewrite !permE //. by move: Hs1; rewrite -Hs2 => /perm_inj. * by move: Hs0; rewrite -Hs2 => /perm_inj. * by move: Hs0; rewrite -Hs1 => /perm_inj. move=> -[-> // | [-> // | [-> // | ]]]. have K1 : P S3.p021 by rewrite (_ : S3.p021 = S3.p01 * S3.p02)%g //; exact/H. have K2 : P S3.p12. rewrite -(_ : S3.p02 * S3.p021 = S3.p12)%g; first exact: H. apply/permP => i. case/or3P : (ord3 i) => /eqP ->; by repeat rewrite !permE /=. have K3 : P S3.p012 by exact: H. by move=> -[-> // | [-> // | -> //]]. 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