proposition: Lemma ofg_Mlt_lto_p2 X: fgraph X -> fg_Mlt_lto X -> limit_ordinal (domain X) -> ofg_Mle_leo X.
proof: Proof. move => p1 p2 p3; move: (ofg_Mlt_lto_p1 p1 p2 p3) => p5. have p51: (forall u, inc u (domain X) -> ordinalp (Vg X u)). by move => u ud; move: (p5 _ ud) => [_ [[ok _] _]]. split => // u v ud vd uv. case: (equal_or_not u v) => nuv. - by move: (p51 _ ud) => h; rewrite -nuv; apply: oleR. - exact (proj1 (p2 _ _ ud vd (conj uv nuv))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)