proposition: Lemma patch_connected_r : connected G -> Gr -> connected Gr.
proof: Proof. move=> ccG xr; rewrite /connected oaGr -(@eq_n_comp_r _ _ G) // => y. apply/esym/exists_inP; exists (hr xr) => /=; last exact: codom_f. by rewrite inE -clink_glink; apply/connectP/connected_clink. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)