proposition: Lemma permS01 n : n <= 1 -> all_equal_to (1 : 'S_n).
proof: Proof. by case: n => [|[|]//=] _ g; rewrite (permS0, permS1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)