proposition: Lemma plainP A : reflect {in A, forall x, edge (edge x) = x /\ edge x != x} (plainb A).
proof: Proof. apply: (iffP subsetP) => plainA x Ax. have oEx: order edge x = 2 by apply/eqP; apply: plainA. split; first by rewrite -{2}(iter_order edgeI x) oEx. by have:= orbit_uniq edge x; rewrite /orbit oEx /= andbT inE eq_sym. have [eex_x x'ex] := plainA x Ax. have Ce2x: fcycle edge [:: x; edge x] by rewrite /= eex_x !eqxx. by apply/eqP/(order_cycle Ce2x); rewrite ?mem_head //= andbT inE eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)