proposition: Lemma le_upper_trans : forall x y z, le_upper x y -> le_upper y z -> le_upper x z.
proof: Proof. intros x y z. case z. split. intro zr. case y. intros _ H. elim H. intros yr. case x. intros H _. elim H. intros xr. simpl. apply Rle_trans. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal