proposition: Theorem discri8: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. case (Rle_or_lt 0%R dp); intros H;[case H; clear H; intros H|idtac]. case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac]. apply discri5; auto with real. apply Rle_lt_trans with (dp*0)%R;[right;ring|auto with real]. unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto. exists dp; split; auto. fold radix; fold FtoRradix; rewrite <- H'; ring. apply discri6; auto. unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto. exists (Fopp dq); split; auto with zarith. apply oppBounded; easy. rewrite Fopp_correct; fold radix; fold FtoRradix; rewrite <- H; ring. case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac]. apply discri7; auto. unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto. exists dp; split; auto. fold radix; fold FtoRradix; rewrite <- H'; ring. apply discri5; auto. apply Rle_lt_trans with (-dp*0)%R;[right;ring|idtac]. apply Rlt_le_trans with ((-dp)*(-dq))%R;[auto with real|right;ring]. Qed.
imports: Reals ZArith List PeanoNat Psatz