proposition: Lemma Midpoint_aux: (FtoRradix x1= f) \/ (exists v:float, (FtoRradix v=x2)%R /\ (Fexp x1 -2 <= Fexp v)%Z).
proof: Proof. case (Rle_or_lt 0 x1); intros H. case H; clear H; intros H. unfold FtoRradix; apply Midpoint_aux_aux with bo p y; auto. absurd (FtoRradix x1 =0)%R; auto with real. assert (~ is_Fzero x1). apply FnormalNotZero with radix bo; auto. unfold is_Fzero in H0. unfold FtoRradix, FtoR; apply prod_neq_R0; auto with real zarith. apply IZR_neq; auto. apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. elim Midpoint_aux_aux with bo radix p (Fopp x1) (Fopp x2) (Fopp y) (Fopp f); auto. repeat rewrite Fopp_correct; fold FtoRradix; intros; left; auto with real. apply Rmult_eq_reg_l with (-1)%R; auto with real. apply trans_eq with (-x1)%R; [ring| apply trans_eq with (1:=H0);ring]. intros T; elim T; intros v T'; elim T'; intros; clear T T'. right; exists (Fopp v); split. unfold FtoRradix; rewrite Fopp_correct; rewrite H0; rewrite Fopp_correct; ring. simpl; apply Z.le_trans with (2:=H1); simpl; auto with zarith. replace (FtoR radix (Fopp x1) + FtoR radix (Fopp x2))%R with (-(x1+x2))%R. apply ClosestOpp; auto. repeat rewrite Fopp_correct; unfold FtoRradix; ring. replace (FtoR radix (Fopp x1) + FtoR radix (Fopp x2)+ FtoR radix (Fopp y))%R with (-(x1+x2+y))%R. apply ClosestOpp; auto. repeat rewrite Fopp_correct; unfold FtoRradix; ring. rewrite <- MSB_opp; rewrite <- LSB_opp; auto. apply FnormalFop; auto. rewrite Fopp_correct; auto with real. rewrite Fopp_correct; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz