proposition: Lemma method_error : forall t : R, let t2 := t * t in let p := p0 + t2 * (p1 + t2 * p2) in let q := q0 + t2 * (q1 + t2 * q2) in let f := 2 * ((t * p) / (q - t * p) + 1/2) in Rabs t <= 355 / 1024 -> Rabs ((f - exp t) / exp t) <= 23 * pow2 (-62).
proof: Proof. intros t t2 p q f Ht. unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ; interval with (i_bisect t, i_taylor t, i_degree 9, i_prec 70). Qed.
imports: Coq(Reals) Flocq(Core) Gappa(Gappa_tactic) Interval(Tactic)