proposition: Lemma sup_increasing_gen r (W := Zo (\Po (substrate r)) (fun z => has_supremum r z)): order r -> increasing_fun (Lf (supremum r) W (substrate r)) (sub_order W) r.
proof: Proof. move => or. move:(sub_osr W) => [qa qb]. have ax :lf_axiom (supremum r) W (substrate r). by move => t /Zo_P[/setP_P ra rb]; apply: inc_supremum_substrate. split => //; first by hnf; aw; split => //; apply: lf_function. move => a b /sub_gleP [aX bX lab]; rewrite !LfV //. move: aX bX => /Zo_P [/setP_P ra rb] /Zo_P [/setP_P rc rd]. by apply:sup_increasing. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)