proposition: Theorem FmaErr_aux1: (a*x+y=r1+ga+al2)%R.
proof: Proof. generalize gatCorrect; intros H. replace (FtoRradix ga) with (FtoRradix gat). replace (FtoRradix gat) with (be1-r1)%R. rewrite al2Def; rewrite u2Def. apply trans_eq with (a * x + y-0)%R;[ring|rewrite <- Be2Zero]. rewrite be2Def; ring. elim H; intros v H'; elim H'; intros H1 H''; elim H''; intros H2 H3; rewrite <- H1. unfold FtoRradix. apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H1; auto. unfold FtoRradix. apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim gatDef; auto. fold FtoRradix; replace (FtoRradix gat) with (gat+be2)%R; auto with real. rewrite Be2Zero; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz