proposition: Lemma card_ecp (A : finType) : #|ecp_dart A| = #|A|.+2.
proof: Proof. rewrite -(card_image (can_inj (@ecp_cancel _))) -!card_option. by apply: eq_card => u; apply/imageP; exists (ecp_decode u); case: u => [[]|]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)