proposition: Lemma cpadj_proper cp cm : proper_cpmask cp cm -> proper_cpmask cp (cpadj cm cp).
proof: Proof. elim: cp cm => [|s cp IHcp] [mr mk]. by case: mr mk => [|b0 [|b1 [|b2 mr]]] []. case: s => //= [n||]. - move=> m_ok; set cm := Cfmask (rotr n mr) mk. have{m_ok} cm_ok: proper_cpmask cp cm by rewrite /= size_rotr. by case: (cpadj cm cp) (IHcp _ cm_ok) => mr' mk' /=; rewrite size_rot. - case: mr => [|b0 [|b1 [|b2 mr]]] //= m_ok; set cm := Cfmask _ mk. by case: (cpadj cm cp) (IHcp cm m_ok) => [[|a0 [|a2 mr']] mk']. case: mr mk => [|b0 [|b1 mr]] //= [|b1' mk] //= m_ok; set cm := Cfmask _ mk. by case: (cpadj cm cp) (IHcp cm m_ok) => [[|a0 [|a1 [|a2 mr']]] mk']. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)