proposition: Lemma sup_extension_order2 E F T: sub T (sub_functions E 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) -> exists x, [/\ least_upper_bound (opp_order (extension_order E F)) T x, (source x = unionb (Lg T source)), (Imf x = unionb (Lg T (fun u => (Imf u)))) & (graph x) = unionb (Lg T graph)].
proof: Proof. move=> Ts ag. set h := Lg T source. have fp: forall i, inc i (domain h) -> function_prop i (Vg h i) F. rewrite /h/function_prop; aw => i iT; rewrite LgV //. move: (Ts _ iT) => /sfunctionsP. by move => [pa pb pc]. have ag1: forall i j, inc i (domain h) -> inc j (domain h) -> agrees_on ((Vg h i) \cap (Vg h j)) i j. rewrite /h; aw;move=> i j iT jT; rewrite ! LgV//. split; [ by apply: subsetI2l | by apply: subsetI2r | ]. move=> a /setI2_P [ai aj]; by apply: ag. move:(extension_covering fp ag1). set g := (common_ext h id F); move => [[fg sf tg] gg rg vg]. have [oe sr] := (extension_osr E F). have [oo os] := (opp_osr oe). have ssEF: sub_functions E F = substrate (opp_order (extension_order E F)) by ue. have Tso: sub T (substrate (opp_order (extension_order E F))) by aw; ue. have sTe: sub T (substrate (extension_order E F)) by ue. have xss:inc g (sub_functions E F). apply /sfunctionsP;split => //. rewrite sf /h; move=> t /setUb_P; aw; move => [y yT]; rewrite LgV// => ty. by move /sfunctionsP: (Ts _ yT) => [_ yE _]; apply: yE. exists g; rewrite rg gg /h; aw; split => //; apply /(lubP oo Tso); split. hnf;rewrite - ssEF; split => //. move=> y yT; move:(Ts _ yT) => yss. apply/extension_order_P2; split => //. move => t ta; rewrite gg /h; apply /setUb_P; aw; ex_tac;rewrite LgV //. move=> z; rewrite /upper_bound - ssEF; move => [zss hyp]. apply /extension_order_P2; split => //. move=> t; rewrite gg /h;move /setUb_P; aw; move => [y yT];rewrite LgV// => tgg. by move: (hyp _ yT) => /extension_order_P2 [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)