proposition: Lemma embed_valid_contract : valid_contract [::] ccr.
proof: Proof. split; try exact: embed_sparse; rewrite ?disjoint_has // size_map ?mapEh1. by have [[]] := Cred_cc. have [[rc'cc _ _ triad_cc] _] := Cred_cc; rewrite disjoint_has has_sym in rc'cc. move=> {}/triad_cc/existsP[x /= /and3P[ac_x adj3x xA'cc]]. apply/existsP; exists (h1 x); apply/and3P; split=> // [{xA'cc} | {adj3x}]. apply: leq_trans adj3x _; rewrite orbitF_h1 // /orbit. move: (arity x) => n; elim: n => //= n IHn in x ac_x *. apply: leq_add; last by rewrite IHn -?(fclosed1 acF). rewrite -embedE /fband has_map; case: hasP => // [[y cc_y yFex]]. by case: hasP => // [[]]; exists y => //=; apply: cface_h1. apply: contra xA'cc => /subsetP ccAx; apply/subsetP=> y cc_y. have cc_ey: edge y \in insertE cc by apply: ccE. have {}ccAx z: z \in insertE cc -> adj (h1 x) (h1 z). by move=> cc_z; apply/ccAx/map_f. have bc_ey: edge y \in bc by apply: (hasPn rc'cc). have: cface x (node y) || cface x (node (edge y)). rewrite -!(cface_ac_h1 ac_x) (embedN (hasPn rc'cc _ cc_y)) embedN //. by rewrite embedE -!mem_spoke_ring adj11_edge -?embedE ?ccAx. case/orP=> [xFny | xFney]. by apply/adjP; exists (node y); rewrite // /rlink cface1 nodeK. apply/adjP; exists (edge (face y)); last by rewrite /rlink e2c -cface1. by rewrite -{1}[y]e2c -(n3c bc_ey) cface1r !nodeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)