proposition: Lemma extension_orderP E F f g: gle (extension_order E F) g f <-> [/\ inc g (sub_functions E F), inc f (sub_functions E F) & extends g f].
proof: Proof. apply /graph_on_P0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)