proposition: Lemma succ_study (r: relation) x (r' := fun a b => r a b /\ a <> b) (Ap := fun y A => forall t, inc t A <-> [/\ r x t, r t y & t <> x]) (Ax:= fun y => exists A, Ap y A) (Ay := fun y => choose (Ap y)) (ly := fun y => the_least (graph_on r (Ay y))): worder_r r -> (forall y, r' x y -> Ax y) -> [/\ (r x x -> ~ (exists y, r' x y) -> forall t, r t t -> r t x), (forall y, r' x y -> r' x (ly y)) , (forall y, r' x y -> forall t, r' x t -> r (ly y) t) & (forall y y', r' x y -> r' x y' -> ly y = ly y')].
proof: Proof. move => wor; move: (wor) => [[ha hb hc] hd] h2. have h3: forall y, r' x y -> Ap y (Ay y). by move => y /h2 ax; apply: choose_pr. have h4: forall y, r' x y -> inc y (Ay y). move => y ya; move:(h3 _ ya) => h; apply/h. by move: ya => [rxy /nesym xny]; split => //; move: (hc _ _ rxy)=> []. have h5: forall y, r' x y -> has_least (graph_on r (Ay y)). move => y ya; move: (h3 _ ya) (h4 _ ya) => yb yc. apply:hd; [by move => t /yb [/hc []] | ex_tac ]. have h6: forall y, r' x y -> order_on (graph_on r (Ay y)) (Ay y). move => y ya; move: (h3 _ ya) => yb. have rr:{inc (Ay y), reflexive_r r} by move => t /yb [/hc []]. by move:(wordering_pr wor rr) => [[qa _] qb]. have h7:forall y, r' x y -> least (graph_on r (Ay y)) (ly y). move => y ya; move: (h6 _ ya) => [oR sR]; apply: the_least_pr => //. exact: h5. have h8: forall y, r' x y -> r' x (ly y). move => y ya; move: (h7 _ ya); rewrite /least (proj2 (h6 _ ya)). by move =>[ /(h3 _ ya) [ua _ /nesym ub] _]; split. have h9: forall y, r' x y -> forall t, r' x t -> r (ly y) t. move => y ya t ta. move: (h7 _ ya); rewrite /least (proj2 (h6 _ ya)); move => [_ yb]. move: (yb _ (h4 _ ya)) => /graph_on_P1 [_ _ yc]. have ryy:=(proj2 (hc _ _ (proj1 ya))). have rtt:= (proj2 (hc _ _ (proj1 ta))). case: (worderr_total wor ryy rtt) => cyt. exact (ha _ _ _ yc cyt). have: inc t (Ay y) by move:ta => [t1 /nesym t2];apply/(h3 _ ya). by move/yb => /graph_on_P1 [_ _]. split => //. + move => rxx ney t rtt. case:(equal_or_not x t) => exy; first by rewrite exy. case: (worderr_total wor rxx rtt) => // rxt. by case: ney; exists t; split. + move => y y' ya yb. exact (hb _ _ (h9 _ ya _ (h8 _ yb)) (h9 _ yb _ (h8 _ ya))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)