proposition: Lemma ecpN_subproof : cancel3 ecp_edge ecpN_node ecpN_face.
proof: Proof. move=> [||x]; rewrite /= ?eqxx //. case: ifP => x0gt2 /=; last by rewrite x0gt2. by rewrite -(inj_eq nodeI) !edgeK eqxx (negPf x0gt2). rewrite !(inj_eq edgeI) -(canF_eq nodeK). case: ifP => /= [/eqP <- | x0'nx]; first by rewrite nodeK. case: ifP => /= [/eqP Dx | nx0'x]. by rewrite if_neg -Dx eq_sym -(canF_eq nodeK) x0'nx. by rewrite -(inj_eq nodeI) edgeK x0'nx nx0'x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)