proposition: Lemma F_r14 : 'Fix_to_g[r14] = [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
proof: Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r14_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. 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)