proposition: Theorem FmaErr_aux2: (a*x+y=r1+ga+al2)%R.
proof: Proof. elim gatCorrect with bo radix p a x y r1 u1 u2 al1 al2 be1; auto. intros v1 T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'. elim gaCorrect; intros v2 T; elim T; intros H4 H5; clear T. replace (FtoRradix ga) with (FtoRradix v2). rewrite H4; rewrite be2Def; rewrite al2Def; rewrite u2Def; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix v2) with (gat+be2)%R; auto. fold FtoRradix; rewrite H4; assert (FtoRradix gat=be1-r1)%R; auto with real. unfold FtoRradix; rewrite <- H1. apply sym_eq; apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. rewrite H1; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz