proposition: Lemma Fnum_ge_0: forall (f : float beta), (0 <= F2R f)%R -> (0 <= Fnum f)%Z.
proof: Proof. intros f H. case (Zle_or_lt 0 (Fnum f)); trivial. intros H1; contradict H. apply Rlt_not_le. now apply F2R_lt_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits