proposition: Lemma sup_increasing2_gen r X (W := Zo (gfunctions X (substrate r)) (has_sup_graph r)) : order r -> increasing_fun (Lf (sup_graph r) W (substrate r)) (induced_order (order_graph X (substrate r) r) W) r.
proof: Proof. move => or. move: (order_graph_osr X (erefl (substrate r)) or). rewrite /W; set r' := order_graph _ _ _; set G := gfunctions _ _. set W1 := Zo _ _; move => [qa qb]. have s1: sub W1 (substrate r') by rewrite qb; apply: Zo_S. move: (iorder_osr qa s1) => [qv qd]. have ax: lf_axiom (sup_graph r) W1 (substrate r). move => t /Zo_P [/gfunctions_P2 [ma mb mc] ha]. move: (proj1 (sup_graph_pr1 or mc ha)); rewrite iorder_sr //. by move/Zo_S. apply: Zo_S. split => //; first by hnf; aw; split => //; apply: lf_function. move => a b /iorder_gleP [aW1 aw1 la]; rewrite !LfV//. move: aW1 => /Zo_P [/gfunctions_P2 [ma mb mc] ha]. move: aw1 => /Zo_P [/gfunctions_P2 [ma' mb' mc'] ha']. have sd: domain a = domain b by ue. apply:sup_increasing2 => //; rewrite mb. by move/graph_on_P1: la => /proj33. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)