proposition: Theorem delta_inf: (delta <= (/2)*(Fulp bo radix precision d)+ ((/2)*(Fulp bo radix precision p)+(/2)*(Fulp bo radix precision q)))%R.
proof: Proof. unfold delta; rewrite <- Rabs_Ropp. replace (-(d - (b * b' - a * c)))%R with (((p-q)-d)+((b*b'-p)+-(a*c-q)))%R;[idtac|ring]. apply Rle_trans with ((Rabs ((p-q)-d))+(Rabs (b * b' - p + - (a * c - q))))%R; [apply Rabs_triang|idtac]. apply Rplus_le_compat. apply Rmult_le_reg_l with (S (S O)); auto with arith real. apply Rle_trans with (Fulp bo radix precision d). unfold FtoRradix; apply ClosestUlp;auto with zarith. elim Roundd; auto. right; simpl; field; auto with real. apply Rle_trans with ((Rabs (b*b'-p))+(Rabs (-(a*c-q))))%R; [apply Rabs_triang|idtac]. apply Rplus_le_compat. apply Rmult_le_reg_l with (S (S O)); auto with arith real. apply Rle_trans with (Fulp bo radix precision p). unfold FtoRradix; apply ClosestUlp;auto with zarith. elim Roundp; auto. right; simpl; field; auto with real. rewrite Rabs_Ropp; apply Rmult_le_reg_l with (S (S O)); auto with arith real. apply Rle_trans with (Fulp bo radix precision q). unfold FtoRradix; apply ClosestUlp;auto with zarith. elim Roundq; auto. right; simpl; field; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz