proposition: Lemma sup_A x: (forall l, inc l (domain c) -> has_sup_graph r (restr f (Vg c l))) -> (sup_graphp r f x <-> sup_graphp r (Lg (domain c) (fun l => sup_graph r (restr f (Vg c l)))) x).
proof: Proof. move=> alsup. set g:= Lg _ _. have fgg:fgraph g by rewrite /g; fprops. have ranr: forall a, inc a (domain c) -> (sub (range (restr f (Vg c a))) (substrate r)). move => a ac; apply: sub_trans rf; apply: restr_range1 => //. rewrite df => s su; union_tac. have srh: (sub (range g) (substrate r)). move=> t /(Lg_range_P) [b bd st]. move: (sup_graph_pr1 or (ranr b bd) (alsup _ bd)). by rewrite st; move /(lubP or (ranr b bd)) => [[? _] _]. split. move/(sup_graphP or rf fgf) =>[xsr p1 p2]. apply/(sup_graphP or srh fgg); split => //. rewrite /g; aw;move=> a adc; rewrite !LgV //. move: (sup_graph_pr1 or (ranr a adc) (alsup _ adc)). move /(lubP or (ranr a adc))=> [_ ]; apply. split=> // y /funI_P [z /funI_P [s sv ->] ->]; aw; apply: p1. rewrite df; union_tac. move=> z zr hyp. apply: p2 =>// a; rewrite df => /setUb_P [y yd aV]. apply: (@order_transitivity r _ (sup_graph r (restr f (Vg c y))) _ or). move: (sup_graph_pr1 or (ranr y yd) (alsup _ yd)). move/(lubP or (ranr y yd)) => [[ _ p] _]; apply: p. apply /funI_P; exists (J a (Vg f a)); aw; trivial;apply /funI_P; ex_tac. move: hyp; rewrite /g; aw => xx; move: (xx _ yd); rewrite LgV//. move/(sup_graphP or srh fgg) =>[xsr p1 p2]. have dgdc: domain g = domain c by rewrite /g; aw. rewrite dgdc in p1 p2. apply/(sup_graphP or rf fgf); split => //. move=> a; rewrite df => /setUb_P [y yd aV]. move: (p1 _ yd) => aux. apply: (order_transitivity or) aux. move: (sup_graph_pr1 or (ranr y yd) (alsup _ yd)). move /(lubP or (ranr y yd)) => [[_ p] _]; rewrite /g LgV//; apply:p. apply /funI_P; exists (J a (Vg f a)); aw; trivial; apply /funI_P;ex_tac. move=> z zr h; apply: p2 =>//. move=> a ad;rewrite /g LgV //. move: (sup_graph_pr1 or (ranr a ad) (alsup _ ad)). move /(lubP or (ranr a ad)) => [_ p]; apply:p. split=>// y /funI_P [t /funI_P [s sa ->] ->]; aw; apply: h. rewrite df; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)