proposition: Theorem LeZEROFnum : forall x : float, (Fnum x <= 0)%Z -> (x <= 0)%R.
proof: Proof. intros x H'; unfold FtoRradix, FtoR in |- *. apply Ropp_le_cancel; rewrite Ropp_0; rewrite <- Ropp_mult_distr_l_reverse. replace 0%R with (- 0%Z * 0)%R; try ring. apply Rmult_le_compat; try auto with real. rewrite <- 2!Ropp_Ropp_IZR; apply IZR_le; lia. now apply powerRZ_le, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz