proposition: Theorem sup_A2: (forall l, inc l (domain c) -> has_sup_graph r (restr f (Vg c l))) -> ((has_sup_graph r f <-> has_sup_graph r (Lg (domain c)(fun l => sup_graph r (restr f (Vg c l))))) /\ (has_sup_graph r f -> sup_graph r f = sup_graph r (Lg (domain c) (fun l => sup_graph r (restr f (Vg c l)))))).
proof: Proof. move=> alsup. split; first by apply: sup_A1=>//. move=> hyp; rewrite /sup_graph. set (g:= Lg (domain c) (fun l => sup_graph r (restr f (Vg c l)))). have lu:= (sup_graph_pr1 or rf hyp). rewrite -(supremum_unique or lu (supremum_pr1 or hyp)). move/(sup_A (sup_graph r f) alsup): lu => lug. have lug': least_upper_bound r (range g) (supremum r (range g)). by apply: supremum_pr1 => //; exists (sup_graph r f). by rewrite -(supremum_unique or lug lug'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)