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