proposition: Lemma minimal_counter_example_mirror : forall G, minimal_counter_example G -> minimal_counter_example (mirror G).
proof: Proof. move=> G; do 4![case] => planarG bridge'G plainG cubicG noncolG minG. split; last 1 [by move/colorable_mirror | by []]. split; last by rewrite precubic_mirror. split; last by rewrite plain_mirror. split; last by rewrite bridgeless_mirror. by rewrite planar_mirror. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)