proposition: Lemma fromZ_DN_correct : forall p n, valid_lb (fromZ_DN p n) = true /\ le_lower (toX (fromZ_DN p n)) (Xreal (IZR 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