proposition: Lemma embed_sparse : sparse (insertE ccr).
proof: Proof. move: Cred_cc => [[rc'cc UccN _ _] _]; move: rc'cc UccN. rewrite disjoint_has has_sym /sparse !simple_recI mapEh1 /=. elim: (insertE cc) => //= x p IHp /norP[rc'x rc'p] /andP[pN'x /IHp-> {IHp}//]. rewrite unfold_in has_map {pN'x}(contra _ pN'x) // => /hasP[z p_z /= h1xNz]. apply/hasP; exists z => //; have{p_z} rc'z := hasPn rc'p z p_z. case/connectP: h1xNz => q; elim: q => /= [|y q IHq] in x rc'x *. by move=> _ /embed_inj->. case/andP=> /eqP <-; rewrite -(embedN rc'x) cnode1; apply: IHq. by rewrite -(fclosed1 rcN). 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)