proposition: Lemma extension_order_pr E F f g: gle (opp_order (extension_order E F)) f g -> {inc source f, f =1f g}.
proof: Proof. move/opp_gleP/extension_orderP=> [gs fs et]; exact: (extends_sV et). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)