proposition: Lemma sup_extension_order1 E F T f: sub T (sub_functions E F) -> least_upper_bound (opp_order (extension_order E F)) T f -> forall u v x, inc u T -> inc v T -> inc x (source u) -> inc x (source v) -> Vf u x = Vf v x.
proof: Proof. move=> Ts lef. have [oe sr] := (extension_osr E F). have [oo so] := (opp_osr oe). have sTe: sub T (substrate (extension_order E F)) by ue. have sT:sub T (substrate (opp_order (extension_order E F))) by ue. move: lef => /(lubP oo sT) [[fs ub] hyp] u v x uT vT xs ys. by rewrite (extension_order_pr (ub _ uT) xs) (extension_order_pr (ub _ vT) ys). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)