proposition: Lemma ofg_Mlt_lto_p1 X: fgraph X -> fg_Mlt_lto X -> limit_ordinal (domain X) -> forall u, inc u (domain X) -> (inc (osucc u) (domain X) /\ Vg X u <o Vg X (osucc u)).
proof: Proof. move=> pa pb [pc pd pe] u ud. have lt1:= (oltS (Os_ordinal pc ud)). move: (pe _ ud) => sb. move: (pb _ _ ud sb lt1) => lt2; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)