proposition: Lemma sub_restrict T (e1 e2 : rel T) (A : pred T) : {in A&, subrel e1 e2} -> subrel (restrict A e1) (restrict A e2).
proof: Proof. move => sub x y /=/andP[/andP [xA yA] xy]. by rewrite xA yA sub. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)