proposition: Lemma F_r23 : 'Fix_to_g[r23] = [set x | (col0 x == col1 x) && (col1 x == col4 x) && (col4 x == col5 x)].
proof: Proof. have r23_inv: r23^-1 = r32 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r23_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. by do 3![case: eqVneq; rewrite ?andbF // => <-]. 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)