proposition: Lemma limit_study (r: relation) y B (C := B +s1 y) (R := (graph_on r C)) (x := supremum R B): (forall a, inc a B <-> r a y /\ a <> y) -> worder_r r -> r y y -> [/\ (least_upper_bound R B x /\ r x y), (B = emptyset -> forall t, r t t -> r y t), ( x <> y -> [/\ inc x B, x = the_greatest (graph_on r B), (forall z, r x z -> r z y -> z = x \/ z = y) & (forall z, r z z -> r z x \/ r y z)]) & (x = y -> forall B1, nonempty B1 -> finite_set B1 -> sub B1 B -> inc (the_greatest (graph_on r B1)) B)].
proof: Proof. move => hB wor ryy. move:(wor) => [ [ha hb hc] _]. have hd: {inc B, reflexive_r r} by move => t /hB [/hc []]. have he: {inc C, reflexive_r r}. move => t /setU1_P []; [by apply:hd | by move -> ]. have sBC: sub B C by apply:sub_setU1. have yC: inc y C by rewrite /C; fprops. have srB:= (graph_on_sr hd). move:(wordering_pr wor he) => [woR sr]. have oR := proj1 woR. have pa: sub B (substrate (graph_on r C)) by rewrite graph_on_sr. have uy: upper_bound (graph_on r C) B y. split; first by rewrite sr. move => t tB;apply /graph_on_P1; split => //; first by apply sBC. by move/(hB t): tB => []. have hs:has_supremum (graph_on r C) B. by apply:(worder_hassup woR pa); exists y. have xp: least_upper_bound R B x by apply: (supremum_pr1 oR). move:(supremum_pr1 oR hs) => /(lubP oR pa) []; rewrite -/x => h1 h2. move: (h2 _ uy) => /graph_on_P1 [_ _ rxy]. have pb: forall t, inc t B -> r t x. by move => t /(proj2 h1) /graph_on_P1 []. have pc: x <> y -> [/\ inc x B, x = the_greatest (graph_on r B), (forall z, r x z -> r z y -> z = x \/ z = y) & (forall z, r z z -> r z x \/ r y z)]. move => xz. have xB: inc x B by apply/hB. move:(supremum_pr1 oR hs) => /(lubP oR pa) [hh _]. move: hh; rewrite -/x; move => [_ hx]. have orB: order (graph_on r B) by apply: (order_from_rel B (proj1 wor)). have xgr: x = the_greatest (graph_on r B). symmetry;apply: (the_greatest_pr2 orB); hnf; rewrite srB; split => //. move => t tB; move/hB: (tB)=> [qa qb]; apply /graph_on_P1; split => //. by move:(hx _ tB) => /graph_on_P1 []. have hh:forall z, r z z -> r z x \/ r y z. move => z rzz; case (equal_or_not z y) => ezy; first by rewrite ezy; right. case: (worderr_total wor ryy rzz) => czy; first by right. have zB: inc z B by apply/hB. by move: (hx _ zB) => /graph_on_P1 [ _ _ rzx]; left. split => // t t1 t2; case (equal_or_not t y) => ty; first by right. have tB: inc t B by apply /hB. by move:(hx _ tB) => /graph_on_P1 [_ _ t3]; rewrite (hb _ _ t1 t3); left. have pd: B = emptyset -> forall t, r t t -> r y t. move => be t rtt. case (equal_or_not t y) => ty; first by ue. case: (worderr_total wor ryy rtt) => // czy. empty_tac1 t; by apply/hB. split => // exy B1 neB1 fsB1 sb1. have hf : {inc B1, reflexive_r r} by move => t/sb1 /hd. move:(wordering_pr wor hf) => [wos ss]. move:(worder_total wos) => tos. have ss1: sub B1 (substrate (graph_on r B1)) by rewrite ss. move: (finite_subset_torder_greatest tos fsB1 neB1 ss1). rewrite -{2} ss (iorder_substrate (proj1 tos)) => hgt. move:(the_greatest_pr (proj1 tos) hgt) => []; rewrite ss => r0 _. by apply: sb1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)