proposition: Theorem mBFadic_correct3 : forall r : R, In (Fopp (boundR r)) (mBFloat r).
proof: Proof. intros r; unfold mBFloat in |- *. replace (Fopp (boundR r)) with ((fun p : Z * Z => Float (fst p) (snd p)) (Fnum (Fopp (boundR r)), Fexp (Fopp (boundR r)))). apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p)); auto. apply mProd_correct; auto. apply mZlist_correct; auto. unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith. replace (-1)%Z with (- Z_of_nat 1)%Z; auto with zarith. apply Zle_Zopp. unfold pPred in |- *; apply Zle_Zpred; simpl in |- *. apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. unfold pPred in |- *; apply Zle_Zpred; simpl in |- *. red in |- *; simpl in |- *; auto. apply mZlist_correct; auto. unfold boundR, boundNat in |- *; simpl in |- *; lia. case (dExp b); try intros; try rewrite N2Z.inj_pos; auto with zarith arith. auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz