proposition: Lemma cofinality_pr8 x z: ordinalp x -> sub z x -> \osup z = x -> \cf x <=c cardinal z.
proof: Proof. move =>ox zx szx. set r := ordinal_o x. move: (ordinal_o_wor ox) => wor. have sr: substrate r = x by apply: ordinal_o_sr. have sr1: sub z (substrate r) by ue. move: (induced_wor wor sr1) => woz; move: wor => [or _]. have crz: cofinal r z. hnf; rewrite sr;split => // t /(oltP ox) tx. have osx: ordinal_set z by move => u / zx /(Os_ordinal ox). rewrite - szx in tx. move:(olt_sup osx tx) => [a az av]; ex_tac. move: (zx _ az) => ax. move /(oltP (Os_ordinal ox ax)): (av) => ta. move: (ordinal_transitive ox ax ta) => itx. by apply/ordo_leP; split => //; move: av => [[_ _ ok] _]. move:(cofinality_pr2 ox zx crz); rewrite - (cofinality_sd ox). move/ocle1. rewrite (card_card (CS_cofinality ox)). rewrite (cardinal_of_ordinal woz) iorder_sr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)