proposition: Lemma M_correct_aux: forall r, 0 <= r <= /100 -> 2 * r ^ 8 + 15 * r ^ 7 + 50 * r ^ 6 + 97 * r ^ 5 + 120 * r ^ 4 + 97 * r ^ 3 + 50 * r ^ 2 + 15 * r <= 52 * r ^ 2 + 15 * r.
proof: Proof. intros r (H1,H2). case H1; intros K. apply Rplus_le_reg_l with (-15*r - 51*r*r); ring_simplify. apply Rmult_le_reg_l with (/(r*r)). apply Rinv_0_lt_compat. now apply Rmult_lt_0_compat. apply Rle_trans with (2*r ^ 6 + 15 * r ^ 5 + 50 * r ^ 4 + 97 * r ^ 3 + 120 * r ^ 2 + 97 * r -1 ). right; field. now apply Rgt_not_eq. apply Rle_trans with 1. 2: right; field. unfold pow; rewrite Rmult_1_r. interval_intro (/100) upper. assert (J := conj H1 (Rle_trans _ _ _ H2 H)). clear -J. interval. now apply Rgt_not_eq. rewrite <-K. right; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)