proposition: Theorem FSuccNormPos : forall a : float, (0 <= a)%R -> Fnormal radix b a -> Fnormal radix b (FSucc a).
proof: Proof. intros a H' H'0; unfold FSucc in |- *. cut (Fbounded b a); [ intros B0 | apply FnormalBounded with (1 := H'0); auto ]. generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b))); case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto. intros H'3; repeat split; simpl in |- *; auto. rewrite Z.abs_eq; try apply ZltNormMinVnum. apply Zlt_le_weak, nNormPos; auto with zarith. apply Z.le_trans with (m := Fexp a); try apply B0; auto with zarith. rewrite pGivesBound; rewrite Z.abs_eq; auto with zarith. pattern precision at 1 in |- *; replace precision with (1 + pred precision). rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; unfold nNormMin in |- *; auto with zarith. generalize precisionNotZero; case precision; auto with zarith. apply Z.mul_nonneg_nonneg; simpl in |- *; auto with zarith. apply Zlt_le_weak, nNormPos; auto with zarith. intros H'3; generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)). intros H'4; absurd (0 <= Fnum a)%Z; auto. 2: apply LeR0Fnum with (radix := radix); auto with zarith. rewrite H'4; auto. apply Zlt_not_le. replace 0%Z with (- 0)%Z by easy. apply Zlt_Zopp, nNormPos; auto with zarith. intros H'4; repeat split; simpl in |- *; auto with zarith. apply Z.le_lt_trans with (Z.succ (Z.abs (Fnum a))). lia. case (Zlt_next (Z.abs (Fnum a)) (Zpos (vNum b))); auto with zarith arith; try apply B0. intros H1; contradict H'3. unfold pPred in |- *; rewrite H1; rewrite Z.abs_eq; auto with zarith. apply LeR0Fnum with (radix := radix); auto with zarith. apply B0. apply Z.le_trans with (Z.abs (radix * Fnum a)); try apply H'0. case H'0; auto. repeat rewrite Zabs_Zmult. cut (0 <= Fnum a)%Z; [ intros Z1 | apply LeR0Fnum with (radix := radix) ]; auto. rewrite (Z.abs_eq (Fnum a)); auto. rewrite (Z.abs_eq (Z.succ (Fnum a))); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz