proposition: Lemma F_s05 : 'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
proof: Proof. have s05_inv: s05^-1=s05 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s05_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= andbT/col1/col2/col3/col4/col5/col0. by do 2![rewrite eq_sym; case: {+}(_ == _)=> //= ]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)