proposition: Lemma fromZ_UP_correct : forall p n, valid_ub (fromZ_UP p n) = true /\ le_upper (Xreal (IZR n)) (toX (fromZ_UP p n)).
proof: Proof. intros p n. split. easy. rewrite fromZ_correct'. apply Rle_refl. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig