Library Coq.micromega.Lqa
Here, lra stands for linear rational arithmetic
Ltac lra := lra_Q rchecker.
Here, nra stands for non-linear rational arithmetic
Ltac nra :=
xnqa rchecker.
Ltac xpsatz dom d :=
let tac :=
lazymatch dom with
|
Q =>
((
sos_Q rchecker) || (
psatz_Q d rchecker))
|
_ =>
fail "Unsupported domain"
end in tac.
Tactic Notation "psatz"
constr(
dom)
int_or_var(
n) :=
xpsatz dom n.
Tactic Notation "psatz"
constr(
dom) :=
xpsatz dom ltac:(-1).