proposition: Lemma ex9_rels_special: right_directed_on r I -> ex9_rels_ext = graph_on ex9_srel ex9_G.
proof: Proof. move => / ex9_propf ha. set s := (graph_on ex9_srel ex9_G). apply: extensionality; last by apply:ex9_prope. set T:= (Zo (equivalences ex9_G) (eqv_smaller ex9_rels)). have sT: inc s T. apply/Zo_P; split; first by apply/equivalencesP. move => x y; move =>[xG yG ll]; case: ll => ll1. by apply/graph_on_P1; split => //; apply:ex9_propa. by apply:(proj44 (proj1 ha));apply/graph_on_P1; split=> //; apply:ex9_propa. rewrite ex9_rels_ext_minimal => t xt; exact:(setI_hi xt sT). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)