proposition: Theorem FmaErr_aux: (a*x+y=r1+ga+al2)%R.
proof: Proof. case (Req_dec be2 0); intros. unfold FtoRradix; apply FmaErr_aux1 with bo p u1 u2 al1 be1 be2 gat; auto. unfold FtoRradix; apply FmaErr_aux2 with bo p P u1 u2 al1 be1 be2 gat; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz