proposition: Lemma cofinality_prod a b: \0o <o a -> limit_ordinal b -> \cf (a *o b) = \cf b.
proof: Proof. move=> ap bl; symmetry. move: (ap) (bl) => [[_ oa _] _] [ob _ lb]. have oab: ordinalp (a *o b) by fprops. have ta: lf_axiom (oprod2 a) b (a *o b). by move=> t /(oltP ob) tb; apply /(oltP oab); apply: oprod_Meqlt. apply: cofinality_pr5 => //. exists (Lf (oprod2 a) b (a *o b)); last first. by move=> x y xb yb; rewrite !LfV// => h; apply: oprod_Meqlt. split; first (by saw; apply: lf_function); last first. move => t /(oltP oab) tab. have ot:=proj31_1 tab. move: (odivision_exists oa ob tab) => [[oq or p3 [p4 _]] /(oltP ob)]. move => /lb qd; ex_tac; rewrite LfV //. rewrite oprod2_succ // {1}p3; apply: osum_Meqle; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)