proposition: Lemma proper_cpmask1 cp i : proper_cpmask cp (cfmask1 cp i).
proof: Proof. by rewrite /= size_nseq size_mkseq !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)