proposition: Lemma Exercise6_16a r: total_order r -> exists2 X, cofinal r X & (worder (induced_order r X)).
proof: Proof. move => [or tor];move: (Exercise2_2b or) => [X [Xsr worX ub]]. exists X => //; split => // x xsr. case: (inc_or_not x X) => xX; first by ex_tac; order_tac. ex_middle h; case: xX; apply: ub. split => // z zX; case: (tor _ _ xsr (Xsr _ zX)) => //. move=> xz; case: h; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)