proposition: Theorem FSuccDiffPos : forall x : float, (0 <= x)%R -> Fminus radix (FSucc b radix precision x) x = Float 1 (Fexp x) :>R.
proof: Proof. intros x H. unfold FtoRradix in |- *; apply FSuccDiff1; auto with zarith. contradict H; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H. apply Rlt_not_le. replace 0%R with (0 * powerRZ radix (Fexp x))%R; [ idtac | ring ]. apply Rlt_monotony_exp; auto with real arith. assert (0 < nNormMin radix precision)%Z. apply nNormPos; auto with zarith. replace 0%R with (IZR (- 0)); auto with real zarith arith. apply IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz