proposition: Lemma cofinality_pr2 x (r:= ordinal_o x) z: ordinalp x -> sub z x -> cofinal r z -> (cofinality_alt x) <=o ordinal (induced_order r z).
proof: Proof. move => /ordinal_o_wor; rewrite -{2} (ordinal_o_sr x);apply:cofinality'_pr3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)