Library Coq.nsatz.Nsatz
Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.
Require Export Integral_domain.
Require Import DiscrR.
Require Import ZArith.
Require Import Lia.
Require Export NsatzTactic.
Make use of discrR in nsatz
Ltac nsatz_internal_discrR ::= discrR.
Require Export Rbase.
Require Export Rfunctions.
Require Import RealField.
Lemma Rsth : Setoid_Theory R (@eq R).
#[global]
Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
Defined.
#[global]
Instance Rri : (Ring (Ro:=Rops)).
Defined.
Ltac extra_reify term ::=
match term with
| IZR ?z =>
match isZcst z with
| true => open_constr:((true, PEc z))
| false => open_constr:((false,tt))
end
| _ => open_constr:((false,tt))
end.
Lemma R_one_zero: 1%R <> 0%R.
#[global]
Instance Rcri: (Cring (Rr:=Rri)).
#[global]
Instance Rdi : (Integral_domain (Rcr:=Rcri)).
Defined.
Require Export Rbase.
Require Export Rfunctions.
Require Import RealField.
Lemma Rsth : Setoid_Theory R (@eq R).
#[global]
Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
Defined.
#[global]
Instance Rri : (Ring (Ro:=Rops)).
Defined.
Ltac extra_reify term ::=
match term with
| IZR ?z =>
match isZcst z with
| true => open_constr:((true, PEc z))
| false => open_constr:((false,tt))
end
| _ => open_constr:((false,tt))
end.
Lemma R_one_zero: 1%R <> 0%R.
#[global]
Instance Rcri: (Cring (Rr:=Rri)).
#[global]
Instance Rdi : (Integral_domain (Rcr:=Rcri)).
Defined.