proposition: Theorem AxpyPos : Fcanonic radix b u -> Fcanonic radix b t -> (0 < u)%R -> (4 * Rabs t <= Rabs u)%R -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) < / 4 * Fulp b radix precision (FPred b radix precision u))%R -> MinOrMax radix b (a1 * x1 + y1) u.
proof: Proof. intros H1 H2 H3 H4 H5. case H2; intros H6. apply Axpy_aux1; auto; apply Axpy_aux1_aux1; auto. cut (forall z1 z2 : Z, (z1 <= z2)%Z -> z1 = z2 \/ (Z.succ z1 <= z2)%Z); [ intros V | idtac ]. 2: intros z1 z2 V; lia. case (V (- dExp b)%Z (Fexp u)); [ elim Fu; intuition | intros H7 | intros H7 ]. apply Axpy_aux2; auto. unfold FtoRradix in |- *; apply plusExact1 with b precision; auto with zarith. rewrite <- H7; elim H6; intros H8 H9; elim H9; intros H10 H11; rewrite H10. rewrite Z.min_l; auto with zarith; elim Fy; auto. case (V (- dExp b)%Z (Fexp (FPred b radix precision u))). cut (Fbounded b (FPred b radix precision u)); [ intros H8 | idtac ]; auto. apply H8. apply FBoundedPred; auto with zarith. intros H8; apply Axpy_aux3; auto. intros H8; apply Axpy_aux1; auto. apply Axpy_aux1_aux3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz