proposition: Lemma patch_gcomp : patch gcompd gcompr [::] [::].
proof: Proof. do ?split; do [by [] | apply: val_inj | ] => // x; rewrite !inE /= orbF. by rewrite codom_gcompd codom_gcompr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)