proposition: Theorem FPredSimpl3 : FPred (Float (nNormMin radix precision) (- dExp b)) = Float (Z.pred (nNormMin radix precision)) (- dExp b).
proof: Proof. unfold FPred 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'0; absurd (0 < pPred (vNum b))%Z; auto with zarith arith. rewrite <- (Z.opp_involutive (pPred (vNum b))); rewrite <- H'0. apply Zle_not_lt; replace 0%Z with (- (0))%Z; [ apply Zle_Zopp | simpl in |- *; auto ]. apply Zlt_le_weak; apply nNormPos; auto with zarith. unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *; auto with zarith. simpl in |- *; apply vNumbMoreThanOne with (3 := pGivesBound); auto. 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