proposition: Lemma Exercise2_6e a b: inc a (source f) -> least_upper_bound r (chainx a) b -> (inc b (chainx a) /\ Vf f b = b).
proof: Proof. move=> asf leb. move: (Exercise2_6c asf) => aca. move:(Exercise2_6d asf) => /Zo_P [p1 [p2] aux]; move: p1 => /setP_P p1. have neca: nonempty (chainx a) by exists a. have ba: inc b (chainx a) by apply: (aux _ _ (@sub_refl (chainx a)) neca leb). split => //; move: leb => /(lubP or p1) [[_ ub] _ ]. move: (ub _ (p2 _ ba)) (fxx (p1 _ ba)) => le1 le2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)