proposition: Lemma segments_numerables r: let r' := fun x => induced_order r (segment r x) in worder r -> (forall x, inc x (substrate r)-> numerable (r' x)) -> numerable r.
proof: Proof. move=> r' wor aln. set f:= (fun x => choose (fun y=> numeration (r' x) y)). have fp: forall x, inc x (substrate r) -> numeration (r' x) (f x). by move=> x xsr; move: (aln _ xsr)=> [_ c];rewrite /f;apply: choose_pr. have or: order r by fprops. have restrp: forall x y, glt r y x -> f y = restr (f x) (substrate (r' y)). move=> x y ryx. have sss: sub (segment r x) (substrate r) by apply: sub_segment. have ssy: sub (segment r y) (substrate r) by apply: sub_segment. have p6: worder (r' y) by apply: induced_wor =>//. apply: (numeration_unique p6); first by apply: fp; order_tac. have <-: (segment (r' x) y) = substrate (r' y). rewrite /r' iorder_sr // segment_induced_a //; last by apply/segmentP. by apply:segment_segment. have p1: worder (r' x) by rewrite /r'; apply: induced_wor =>//. have p2: numeration (r' x) (f x) by apply: fp; order_tac. have p3: inc y (substrate (r' x)) by rewrite /r' iorder_sr //; apply /segmentP. move: (sub_numeration p1 p2 p3). have -> //: induced_order (r' x) (segment (r' x) y) = r' y. rewrite /r' segment_induced // iorder_trans //. apply: (segment_monotone or (proj1 ryx)). have gp: forall x y, glt r y x -> range (f y) = Vg (f x) y. move=> x y yx. have xsr: (inc x (substrate r)) by order_tac. have ysr: (inc y (substrate r)) by order_tac. move: (fp _ xsr) => [fg df vf]. move: df; rewrite /r' iorder_sr // => df; last by apply: sub_segment. have ysrx: (inc y (segment r x)) by apply /segmentP. rewrite df in vf; rewrite (vf _ ysrx) (restrp _ _ yx). have ->: (segment (r' x) y) = (substrate (r' y)). rewrite /r' iorder_sr //;[ by rewrite segment_induced | apply: sub_segment]. have gr: sgraph (restr (f x) (substrate (r' y))) by fprops. have fgr: fgraph (restr (f x) (substrate (r' y))) by fprops. have hh: sub (substrate (r' y)) (domain (f x)). rewrite df; rewrite /r' (iorder_sr or (@sub_segment r y)). apply:(segment_monotone or (proj1 yx)). set_extens u. move /(range_gP fgr); aw; move => [z pa pb]; apply /dirim_P; exists z => //. by move: pb; rewrite LgV// => ->; apply:(fdomain_pr1 fg); apply: hh. move /dirim_P => [z za zb];apply /(range_gP fgr); exists z; aw; trivial. by move: (pr2_V fg zb); rewrite LgV//; aw. split =>//; exists (Lg (substrate r) (range \o f)). red; aw; split;fprops. move=> x xsr; rewrite LgV//. move: (fp _ xsr) => [ff df vf]. move: df; rewrite /r' iorder_sr // => df; last by apply: sub_segment. have gf: sgraph (f x) by fprops. have p0: sub (segment r x) (substrate r) by apply: sub_segment. have fgL: fgraph (Lg (substrate r) (range \o f)) by fprops. set_extens t. move=> /(range_gP ff) [z pa pb]; apply /dirim_P; exists z; first ue. move: pa; rewrite df => /segmentP h; rewrite pb - (gp _ _ h); apply: Lg_i. order_tac. move /dirim_P => [z xs JL]; move: (p0 _ xs) => zs. move /segmentP: (xs) => lt1. move: (pr2_V fgL JL); aw; rewrite LgV// => -> /=; rewrite (gp _ _ lt1). by apply /(range_gP ff); exists z => //; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)