proposition: Lemma ofg_Mle_leo_p1 X: fgraph X -> fg_Mle_leo X -> ordinalp (domain X) -> ofg_Mle_leo X.
proof: Proof. move => pa pb pc; split => //. move=> x xi; move: (oleR (Os_ordinal pc xi)) => xx. apply: (proj31 (pb _ _ xi xi xx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)