proposition: Lemma cofinality_sum a b: ordinalp a -> \0o <o b -> \cf (a +o b) = \cf b.
proof: Proof. move=> oa bnz; symmetry. have b0: inc \0o b by move/oltP0:bnz => []. have ob:= proj32_1 bnz. have oab: ordinalp (a +o b) by fprops. have ta: lf_axiom (osum2 a) b (a +o b). by move=> t /(oltP ob) tb; apply /(oltP oab); apply: osum_Meqlt. apply: cofinality_pr5 => //. exists (Lf (osum2 a) b (a +o b)); last first. by move=> x y xb yb; rewrite !LfV// => h; apply: osum_Meqlt. split;first by saw; apply: lf_function. move => t /(oltP oab) tab; move:(proj31_1 tab) => ot. case: (oleT_ee ot oa) => lta. ex_tac; rewrite LfV //;by rewrite (osum0r oa). move: (odiff_pr lta)=> [da db]. have b1: inc (t -o a) b. by apply /(oltP ob); apply: (osum_Meqltr da ob oa); rewrite - db. ex_tac; rewrite LfV// - db; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)