proposition: Lemma upper_bounds1_P x y r: order r -> inc x (substrate r) -> inc y (substrate r) -> (gle r x y <-> sub (upper_bounds1 r y) (upper_bounds1 r x)).
proof: Proof. rewrite /upper_bounds1 => or xs ys;split. move=> lexy t /Zo_P [ts yt]; apply :Zo_i => //;order_tac. set s:= Zo _ _; move=> ss. have yss: inc y s by rewrite /s Zo_P; split => //; order_tac. by move /Zo_P: (ss _ yss)=> []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)