proposition: Lemma add_edge_adjn u v : adjn (Icp u : H) (Icp v) = [|| adjn u v , cnode u x && cnode v y | cnode u y && cnode v x].
proof: Proof. apply/exists_inP/idP => [[[||z]]|]; rewrite ?inE; last case/or3P. - by rewrite [_ (Icp u) _]cnode1r [_ (Icp v) _]cnode1r !add_edge_cnodeE -!cnode1r => -> ->. - by rewrite [_ (Icp u) _]cnode1r [_ (Icp v) _]cnode1r !add_edge_cnodeE -!cnode1r => -> ->. - rewrite !add_edge_cnodeE => ? ?; rewrite (_ : adjn u v = true) //. by apply/exists_inP; exists z. - by case/exists_inP => z; rewrite !inE -!add_edge_cnodeE => ? ?; exists (Icp z). - rewrite -!add_edge_cnodeE [_ _ (Icp x)]cnode1r [_ _ (Icp y)]cnode1r /=. rewrite !eqxx eq_sym (negbTE xDy) => /andP [? ?]. by exists IcpX. - rewrite -!add_edge_cnodeE [_ _ (Icp x)]cnode1r [_ _ (Icp y)]cnode1r /=. rewrite !eqxx eq_sym (negbTE xDy) => /andP [? ?]. by exists IcpXe. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)