proposition: Lemma increasing_function_segments r r' f g: worder r -> worder r' -> increasing_fun f r r' -> strict_increasing_fun g r r'-> segmentp r' (Imf f) -> forall x, inc x (source f) -> gle r' (Vf f x) (Vf g x).
proof: Proof. move=> wor wor' [or or' [ff sf tf] incf] [_ _ [fg sg tg] sing] sr x xsf. set (s :=Zo (source f) (fun x => (glt r' (Vf g x) (Vf f x)))). have sfsg: source f = source g by ue. move: (worder_total wor) => tor. move: (worder_total wor') => tor'. have Wfsr': inc (Vf f x) (substrate r') by rewrite - tf; fprops. have Wgsr': inc (Vf g x) (substrate r'). by rewrite sfsg in xsf;rewrite - tg; fprops. case: (total_order_pr2 tor' Wgsr' Wfsr') =>// Wlt. have nes: nonempty s by exists x; rewrite /s; apply: Zo_i. have ssf: sub s (substrate r) by rewrite /s sf; apply: Zo_S. move:(worder_prop wor ssf nes)=> [y ys yle]. move: ys => /Zo_P [ysf [leWy neWy]]. have Wrg: inc (Vf f y) (Imf f) by Wtac. move: ((proj2 sr) _ _ Wrg leWy). move/(Imf_P ff) => [z zf vv]. have lt1: glt r' (Vf f z) (Vf f y) by rewrite - vv. have lt2: glt r z y. have: (glt r z y \/ gle r y z). rewrite sf in ysf zf; apply: (total_order_pr2 tor zf ysf). case =>// yz; move: (incf _ _ yz)=> lt4; order_tac. have Wzf: inc (Vf f z) (substrate r') by rewrite - tf; fprops. have Wzg: inc (Vf g z) (substrate r') by rewrite sfsg in zf;rewrite- tg; fprops. case: (total_order_pr2 tor' Wzg Wzf) => h. have zs: (inc z s) by apply: Zo_i. case: (not_le_gt or (yle _ zs) lt2). move: (sing _ _ lt2); rewrite vv => lt3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)