proposition: Lemma size_ctrmask cp cci : size (ctrmask cp cci) = ctrmsize cp.
proof: Proof. by rewrite /ctrmask; elim: (ctrmsize cp) 0 => //= *; congr _.+1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)