proposition: Lemma least_extension E F: least (opp_order (extension_order E F)) (empty_function_tg F).
proof: Proof. have [or sr] :=(extension_osr E F). hnf;move: (opp_osr or) => [or' ->]; rewrite sr. have p1:inc (empty_function_tg F) (sub_functions E F). have [pa pb pc] := (empty_function_tg_function F). apply/sfunctionsP; split => //; rewrite pb; fprops. split=>// x xs; apply/igraph_pP /extension_order_P1; split => //. rewrite empty_function_graph; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)