proposition: Lemma inf_graphP r f: order r -> sub (range f) (substrate r) -> fgraph f -> forall x, (inf_graphp r f x <-> [/\ inc x (substrate r), (forall a, inc a (domain f) -> gle r x (Vg f a)) & forall z, inc z (substrate r) -> (forall a, inc a (domain f) -> gle r z (Vg f a)) -> gle r z x]).
proof: Proof. move=> or sr fg. have gf: sgraph f by fprops. split. move/(glbP or sr) => [[pa pb] pc]; split => //. by move=> a ad; apply: pb;fprops. move=> z zs p; apply: pc; split => //. move=> y /(rangeP gf) [t Jg]. by move: (pr2_V fg Jg); aw; move=> ->; apply: p; ex_tac. move=> [xs p1 p2]; apply /(glbP or sr); split. split=>//; move=> y /(rangeP gf) [z Jg]; move: (pr2_V fg Jg); aw. move=> ->; apply: p1; aw; ex_tac. move=> z [zr p3]; apply: p2 =>//; move=> a ad; apply: p3; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)