proposition: Lemma extension_order_P1 E F f g: gle (extension_order E F) g f <-> [/\ inc g (sub_functions E F), inc f (sub_functions E F) & sub (graph f) (graph g)].
proof: Proof. split; first by move/extension_orderP => [pa pb [_ _ pd _]]. move=> [p1 p2 sh]; apply/extension_orderP; split=>//. move: p1 p2 => /sfunctionsP [fg _ tg] /sfunctionsP [ff _ tf]. split => //; rewrite tg tf;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)