title: In Coq, are there tactics for working with Rabs, Rineq?
body: <p>I am new to Coq, and my primary interest is in using it to do simple real analysis problems.  For a first exercise, I managed to bash through a proof that x^2+2x tends to 0 as x tends to 0.  See code below.</p>
  
  <p>This seems pretty clunky, and I would be interested in any general feedback on how to shorten this proof, or good practice for improving its readability.  However, my main question is whether there are any Coq tactics for automating simple tasks involving the real numbers, along the lines of <code>field</code> and <code>lra</code> but better.</p>
  
  <p><strong>possible example 1:</strong>  are there any tactics to prove identities for the functions from <code>Rbasic_fun</code>, such as the absolute value?  For example, half my proof is dedicated to showing that |x*x|+|2*x|=|x|<em>|x|+2</em>|x| !</p>
  
  <p><strong>possible example 2:</strong> are there any tactics to automate the use of the lemmas from <code>Rineq</code>, such as <code>Rlt_le</code>, <code>Rle_trans</code>, <code>Rplus_le_compat_r</code> and <code>Rmult_le_compat_r</code>?  That is, lemmas that a human proof-creator would use to "chain together" a sequence of inequalities.</p>
  
  <pre><code>Require Import Rbase.
  Require Import Rbasic_fun.
  Require Import Lra.
  Local Open Scope R_scope.
  
  Definition limit (f:R -&gt; R)
    (D:R -&gt; Prop) (l:R) (x0:R) :=
    forall eps:R,
      eps &gt; 0 -&gt;
      exists delta : R,
        delta &gt; 0 /\
        (forall x:R, D x /\ Rabs (x - x0) &lt; delta -&gt; Rabs ((f x) - l) &lt; eps).
  
  Lemma limitf : limit (fun (x:R) =&gt; x*x + 2 *x) (fun x =&gt; True) 0 0.
  Proof.
    unfold limit; intros.
    split with (Rmin (eps/3) 1); split.
    assert (eps / 3 &gt; 0) by lra; clear H.
    assert (1&gt;0) by lra.
    apply (Rmin_Rgt_r (eps/3) 1). apply (conj H0 H).
    intros. destruct H0. clear H0.  replace (x-0) with x in H1 by field.
    apply (Rmin_Rgt_l (eps/3) 1) in H1. destruct H1.
    assert (Rabs (x*x+2*x -0) &lt;= Rabs(x*x)+Rabs(2*x)).
      replace (x*x+2*x-0) with (x*x+2*x) by field.
      apply Rabs_triang.
    assert (Rabs(2*x) =  2 * Rabs(x)). 
      assert (Rabs(2*x) =  Rabs(2) * Rabs(x)).
        apply (Rabs_mult _ _).
      assert (Rabs 2 = 2).
        apply (Rabs_right _). lra.
      replace (Rabs 2) with 2 in H3 by H4. apply H3.
    replace (Rabs (2 * x)) with (2 * Rabs x) in H2 by H3.  clear H3.
    assert (Rabs(x*x) = Rabs(x)*Rabs(x)). 
      apply Rabs_mult.
    replace (Rabs(x*x)) with (Rabs(x)*Rabs(x)) in H2 by H3.  clear H3.
    assert (Rabs x * Rabs x &lt;= 1 * Rabs x).
      apply Rmult_le_compat_r.  apply Rabs_pos.  apply Rlt_le. auto.
    apply (Rplus_le_compat_r (2 * Rabs x) _ _) in H3.
    apply  (Rle_trans _ _ _ H2) in H3. clear H2.
    replace (1 * Rabs x + 2 * Rabs x) with (3 * Rabs x) in H3 by field.
    assert (3 * Rabs x &lt; eps) by lra.
    apply  (Rle_lt_trans _ _ _ H3). auto.
  Qed.
  </code></pre>