proposition: Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.
proof: Proof. apply/setP/subset_eqP/andP; split; first last. rewrite gen_subG; apply/subsetP. by move=> x /[!inE] /orP[] /eqP->; rewrite !eqxx !orbT. apply/subsetP => x /[!inE]. have -> : s05 = r05 * r05 by iso_tac. have -> : s14 = r14 * r14 by iso_tac. have -> : s23 = r14 * r14 * r05 * r05 by iso_tac. have -> : r23 = r05 * r14 * r05 * r14 * r14 by iso_tac. have -> : r50 = r05 * r05 * r05 by iso_tac. have -> : r41 = r14 * r14 * r14 by iso_tac. have -> : r32 = r14 * r14 * r14 * r05* r14 by iso_tac. have -> : r024 = r05 * r14 * r14 * r14 by iso_tac. have -> : r042 = r14 * r05 * r05 * r05 by iso_tac. have -> : r012 = r14 * r05 by iso_tac. have -> : r021 = r05 * r14 * r05 * r05 by iso_tac. have -> : r031 = r05 * r14 by iso_tac. have -> : r013 = r05 * r05 * r14 * r05 by iso_tac. have -> : r043 = r14 * r14 * r14 * r05 by iso_tac. have -> : r034 = r05 * r05 * r05 * r14 by iso_tac. have -> : s1 = r14 * r14 * r05 by iso_tac. have -> : s2 = r05 * r14 * r14 by iso_tac. have -> : s3 = r05 * r14 * r05 by iso_tac. have -> : s4 = r05 * r14 * r14 * r14 * r05 by iso_tac. have -> : s5 = r14 * r05 * r05 by iso_tac. have -> : s6 = r05 * r05 * r14 by iso_tac. by do ?case/predU1P=> [<-|]; first exact: group1; last (move/eqP<-); rewrite ?groupMl ?mem_gen // !inE eqxx ?orbT. 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)