proposition: Fact ecpA_subproof : cancel3 ecpA_edge ecpA_node ecpA_face.
proof: Proof. move=> x; rewrite /ecpA_edge /ecpA_face; case: ifP => ->; rewrite /= /ecpA_node. have [-> | /negPf x0'x] := altP (x =P x0); first by rewrite nodeK eqxx. rewrite -fun_if edgeK (canF_eq (canF_sym nodeK)). by have [<- | /negPf ->] := altP (x =P _); rewrite ?(eqxx, eq_sym x0) x0'x. rewrite (inj_eq edgeI) -!fun_if !(canF_eq (canF_sym nodeK)). have [-> | /negPf x0'x] := altP (x =P x0); first by rewrite eqxx. rewrite edgeK (canF_eq (canF_sym nodeK)). have [Dx | /negPf ->] := altP (x =P _); last by rewrite x0'x edgeK. by rewrite eqxx -Dx eq_sym x0'x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)