proposition: Lemma cofinal_trans r x y: order r -> cofinal r x -> cofinal (induced_order r x) y -> cofinal r y.
proof: Proof. move=> or [xsr cx]; move /(cofinal_inducedP or xsr). move=> [yx xy]; split; first by apply: sub_trans xsr. move=> t tx; move: (cx _ tx) => [z zx zy]. move: (xy _ zx) => [u uy zu]; ex_tac; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)