proposition: Lemma upper_bounds1_decreasing r: order r -> strict_decreasing_fun (Lf (upper_bounds1 r) (substrate r)(\Po (substrate r))) r (subp_order (substrate r)).
proof: Proof. move=> or; hnf; aw; aw. set E:= substrate r. have [oe si] :=(subp_osr E). have ta: lf_axiom (upper_bounds1 r) E (\Po E). by move=> x xE; apply /setP_P => t /Zo_P []. split => //. by rewrite si;saw; apply: lf_function. move => x y ltxy. have xE: inc x E by rewrite /E;order_tac. have yE: inc y E by rewrite /E;order_tac. have [lexy nxy] := ltxy. move:(lexy) => /(upper_bounds1_P or xE yE) sxy. rewrite !LfV //; split. apply /subp_gleP;split => //. by move: (ta _ yE) =>/setP_P. by move: (ta _ xE) =>/setP_P. dneg seq. suff: gle r y x by move => le; order_tac. by apply/(upper_bounds1_P or yE xE) ;rewrite seq; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)