proposition: Theorem FSuccSimpl3 : FSucc (Float (- nNormMin radix precision) (- dExp b)) = Float (Z.succ (- nNormMin radix precision)) (- dExp b).
proof: Proof. unfold FSucc in |- *; simpl in |- *. generalize (Z_eq_bool_correct (- nNormMin radix precision) (pPred (vNum b))); case (Z_eq_bool (- nNormMin radix precision) (pPred (vNum b))); auto. intros H'1; absurd (0 <= pPred (vNum b))%Z; auto with zarith arith. rewrite <- H'1. unfold nNormMin in |- *; simpl in |- *; auto with zarith. replace 0%Z with (- (0))%Z; auto with zarith. now apply Zlt_not_le, Zlt_Zopp, Zpower_nat_less. unfold pPred in |- *; apply Zle_Zpred; auto with zarith. intros H'; generalize (Z_eq_bool_correct (- nNormMin radix precision) (- nNormMin radix precision)); case (Z_eq_bool (- nNormMin radix precision) (- nNormMin radix precision)). intros H'0; generalize (Z_eq_bool_correct (- dExp b) (- dExp b)); case (Z_eq_bool (- dExp b) (- dExp b)); auto. intros H'1; contradict H'1; auto. intros H'1; contradict H'1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz