proposition: Lemma cofinal_inducedP u: sub u (substrate r) -> forall v, cofinal (induced_order r u) v <-> (sub v u /\ (forall x, inc x u -> exists2 y, inc y v & gle r x y)).
proof: Proof. move=> usr v; rewrite /cofinal iorder_sr//. split; move=> [vu h]; split => //; move=> x xu; move: (h _ xu)=> [y yv yx]. ex_tac; apply: (iorder_gle1 yx). by ex_tac; apply /iorder_gle0P => //; apply: vu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)