CoRN.tactics.Qauto

Require Export Qordfield.
Require Import COrdFields2.
Require Import Qpower.
Require Import Qabs.
Require Import CornTac.

Ltac Qauto_pos :=
  repeat (first [ assumption
                | constructor
                | apply Q.Qplus_pos_compat
                | apply Q.Qmult_lt_0_compat
                | apply Qinv_lt_0_compat]);
  auto with ×.

Ltac Qauto_nonneg :=
  repeat (first [assumption
               |discriminate
               |apply: Qabs_nonneg
               |apply: Qsqr_nonneg
               |apply: plus_resp_nonneg;simpl
               |apply: mult_resp_nonneg;simpl
               |apply: Qle_shift_div_l;[Qauto_pos|ring_simplify]
               |apply: Qle_shift_inv_l;[Qauto_pos|ring_simplify]]);
  auto with ×.

Ltac Qauto_le :=
 rewrite → Qle_minus_iff;ring_simplify;Qauto_nonneg.