proposition: Lemma F_r012 : 'Fix_to_g[r012] = [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x) && (col4 x == col5 x)].
proof: Proof. have r012_inv: r012^-1 = r021 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r012_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. 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)