proposition: Lemma sup_increasing2 r f f': order r -> fgraph f -> fgraph f' -> domain f = domain f' -> sub (range f) (substrate r) -> sub (range f') (substrate r) -> has_sup_graph r f -> has_sup_graph r f'-> (forall x , inc x (domain f) -> gle r (Vg f x) (Vg f' x)) -> gle r (sup_graph r f) (sup_graph r f').
proof: Proof. move=> or gf gf' df sr sr' hs hs' ale. move /(sup_graphP or sr gf): (sup_graph_pr1 or sr hs) =>[sgr p1 p2]. move /(sup_graphP or sr' gf'): (sup_graph_pr1 or sr' hs') =>[sgr' p1' p2']. apply: p2=>// a ad. apply: (@order_transitivity r _ (Vg f' a) _ or); [apply:ale=>//|apply: p1']; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)