Library Stdlib.setoid_ring.RealField

From Stdlib Require Import PeanoNat.
From Stdlib Require Import BinNat.
From Stdlib Require Import Nnat.
From Stdlib Require Import ArithRing.
From Stdlib Require Export Ring Field.
From Stdlib Require Import Rdefinitions.
From Stdlib Require Import Rpow_def.
From Stdlib Require Import Raxioms.

Local Open Scope R_scope.

Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).

Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).

Lemma Rlt_n_Sn : forall x, x < x + 1.

Notation Rset := (Eqsth R).
Notation Rext := (Eq_ext Rplus Rmult Ropp).

Lemma Rlt_0_2 : 0 < 2.

Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.

Lemma Rgen_phiPOS_not_0 :
  forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.

Lemma Zeq_bool_complete : forall x y,
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
  Z.eqb x y = true.

Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m.

Lemma R_power_theory : power_theory 1%R Rmult (@eq R) N.to_nat pow.

Ltac Rpow_tac t :=
  match isnatcst t with
  | false => constr:(InitialRing.NotConstant)
  | _ => constr:(N.of_nat t)
  end.

Ltac IZR_tac t :=
  match t with
  | R0 => constr:(0%Z)
  | R1 => constr:(1%Z)
  | IZR (Z.pow_pos 10 ?p) =>
    match isPcst p with
    | true => constr:(Z.pow_pos 10 p)
    | _ => constr:(InitialRing.NotConstant)
    end
  | IZR ?u =>
    match isZcst u with
    | true => u
    | _ => constr:(InitialRing.NotConstant)
    end
  | _ => constr:(InitialRing.NotConstant)
  end.

Add Field RField : Rfield
   (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).