proposition: Lemma inf_decreasing_gen r (W := Zo (\Po (substrate r)) (fun z => has_infimum r z)): order r -> decreasing_fun (Lf (infimum r) W (substrate r)) (sub_order W) r.
proof: Proof. move => or. move:(sub_osr W) => [qa qb]. have ax :lf_axiom (infimum r) W (substrate r). by move => t /Zo_P[/setP_P ra rb]; apply: inc_infimum_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:inf_decreasing. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)