proposition: Lemma card_patch : #|Gd| + #|Gr| = size bG + #|G|.
proof: Proof. rewrite -(card_codom Ihd) -(card_codom Ihr) -cardUI (eq_card EhdUr) addnC. by rewrite (eq_card EhdIr) (card_uniqP UbG). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)