proposition: Lemma extension_order_P2 E F f g: gle (opp_order (extension_order E F)) g f <-> [/\ inc g (sub_functions E F), inc f (sub_functions E F) & sub (graph g) (graph f)].
proof: Proof. split; first by move/opp_gleP /extension_order_P1=> []. by move => [pa pb pc]; apply/opp_gleP /extension_order_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)