proposition: Lemma ErrFMA_bounded: format r1 /\ format r2 /\ format r3.
proof: Proof. Proof with auto with typeclass_instances. split. apply generic_format_round... split. apply generic_format_round... replace (r3) with (-(r2-(gamma+alpha2))) by (unfold r3; ring). apply generic_format_opp. apply plus_error... apply generic_format_round... replace (alpha2) with (-(alpha1-(y+u2))) by (unfold alpha2; ring). apply generic_format_opp. apply plus_error... replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... intros L; case V1_Und1; easy. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat