Skip to content

Commit

Permalink
rm natr_def
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Jul 5, 2024
1 parent 758a614 commit 6901bab
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 9 deletions.
2 changes: 1 addition & 1 deletion CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
+ lemma `ge_floor`

- in `mathcomp_extra.v`:
+ lemmas `intr1`, `int1r`, `natr_def`
+ lemmas `intr1`, `int1r`

### Changed

Expand Down
3 changes: 0 additions & 3 deletions classical/mathcomp_extra.v
Original file line number Diff line number Diff line change
Expand Up @@ -383,9 +383,6 @@ Proof. by rewrite intrD. Qed.

From mathcomp Require Import archimedean.

Lemma natr_def (n : int) : (n \is a Num.nat) = (0 <= n)%R.
Proof. by []. Qed.

Section floor_ceil.
Context {R : archiDomainType}.
Implicit Type x : R.
Expand Down
3 changes: 2 additions & 1 deletion theories/Rstruct.v
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
Require Import Rtrigo1 Reals.
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
From mathcomp Require Import archimedean.
From HB Require Import structures.
From mathcomp Require Import mathcomp_extra.

Expand Down Expand Up @@ -87,7 +88,7 @@ Proof. by move=> *; rewrite Rplus_assoc. Qed.
HB.instance Definition _ := GRing.isZmodule.Build R
RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Fact RmultA : associative (Rmult).
Fact RmultA : associative Rmult.
Proof. by move=> *; rewrite Rmult_assoc. Qed.

Fact R1_neq_0 : R1 != R0.
Expand Down
8 changes: 4 additions & 4 deletions theories/ereal.v
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
(* Copyright (c) - 2016--2018 - Polytechnique *)
(* -------------------------------------------------------------------- *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap archimedean.
From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import fsbigop cardinality set_interval.
Require Import reals signed topology.
Expand Down Expand Up @@ -1403,19 +1403,19 @@ Proof.
move=> P; rewrite /ereal_loc_seq.
case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat.
by rewrite natr_def floor_ge0 le_max lexx orbC.
by rewrite Znat_def floor_ge0 le_max lexx orbC.
exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin.
have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx.
apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
by rewrite natr1 mulrz_nat ler_nat.
have /natrP[N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Num.nat.
by rewrite natr_def floor_ge0 le_max lexx orbC.
by rewrite Znat_def floor_ge0 le_max lexx orbC.
exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl.
have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx.
apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
by rewrite natr1 mulrz_nat ler_nat.
have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat.
by rewrite natr_def floor_ge0.
by rewrite Znat_def floor_ge0.
exists N => // n leNn; apply: dP; last first.
by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0.
rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
Expand Down

0 comments on commit 6901bab

Please sign in to comment.