Skip to content

Commit

Permalink
change inequality in ereal_{d,}nbhs
Browse files Browse the repository at this point in the history 
- from strict to large

closed #122
  • Loading branch information
@affeldt-aist
affeldt-aist committed Dec 4, 2021
1 parent 39c80bd commit 5a4a8ea
Show file tree
Hide file tree
Showing 5 changed files with 118 additions and 77 deletions.
7 changes: 7 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,19 @@
+ lemma `setDIr`
+ lemmas `setMT`, `setTM`, `setMI`
+ lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl`
- in `posnum.v`:
+ lemmas `pos_le_maxl`, `pos_le_minr`
- in `ereal.v`:
+ lemmas `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add`

### Changed

- in `normedtype.v`:
+ `nbhs_minfty_lt` renamed to `nbhs_ninfty_lt_pos` and changed to not use `{posnum R}`
+ `nbhs_minfty_le` renamed to `nbhs_ninfty_le_pos` and changed to not use `{posnum R}`
- in `ereal.v`:
+ definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead
of strict inequality

### Renamed

Expand Down
139 changes: 79 additions & 60 deletions theories/ereal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1158,6 +1158,10 @@ move: x y a b => [x| |] [y| |] [a| |] [b| |] _ _ //=;
by rewrite !lte_fin; exact: ltr_le_add.
Qed.

Lemma lee_lt_add a b x y : a \is a fin_num -> b \is a fin_num ->
a <= x -> b < y -> a + b < x + y.
Proof. by move=> afin bin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.

Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u.
Proof.
move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=;
Expand Down Expand Up @@ -2095,6 +2099,18 @@ exists (PosNum xy); apply/negP; rewrite -ltNge lte_fin -ltr_subr_addl.
by rewrite ltr_pdivr_mulr // ltr_pmulr ?subr_gt0 // ltr1n.
Qed.

Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z.
Proof. by move=> *; rewrite -[y]add0e lee_add. Qed.

Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z.
Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed.

Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x.
Proof. by move=> *; rewrite addeC lee_paddl. Qed.

Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x.
Proof. by move=> *; rewrite addeC lte_paddl. Qed.

Lemma lte_spaddr z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.
Proof.
move: z y x => [z| |] [y| |] [x| |] _ //=;
Expand Down Expand Up @@ -2433,14 +2449,14 @@ Local Open Scope classical_set_scope.
Definition ereal_dnbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
match x with
| r%:E => r^' (fun r => P r%:E)
| +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
| -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
| +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
| -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
end.
Definition ereal_nbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
match x with
| x%:E => nbhs x (fun r => P r%:E)
| +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
| -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
| +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
| -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
end.
Canonical ereal_ereal_filter :=
FilteredType (extended R) (extended R) (ereal_nbhs).
Expand Down Expand Up @@ -2469,63 +2485,63 @@ case=> [x||].
by move=> P Q PQ /xS; apply => y /PQ.
- apply Build_ProperFilter.
move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=.
by rewrite lte_fin ltr_addl.
split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
by rewrite lee_fin ler_addl.
split=> /= [|P Q [MP [MPr geMP]] [MQ [MQr geMQ]] |P Q sPQ [M [Mr geM]]].
+ by exists 0%R; rewrite real0.
+ have [MP0|MP0] := eqVneq MP 0%R.
have [MQ0|MQ0] := eqVneq MQ 0%R.
by exists 0%R; rewrite real0; split => // x x0; split;
[apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
[apply/geMP; rewrite MP0 | apply/geMQ; rewrite MQ0].
exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split.
by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin.
by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
by apply: geMP; rewrite (le_trans _ MQx) // MP0 lee_fin.
by apply geMQ; rewrite (le_trans _ MQx)// lee_fin real_ler_normr ?lexx.
have [MQ0|MQ0] := eqVneq MQ 0%R.
exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split.
by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
by apply geMP; rewrite (le_trans _ MPx)// lee_fin real_ler_normr ?lexx.
by apply geMQ; rewrite (le_trans _ MPx) // lee_fin MQ0.
have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
rewrite realE /= posnum_ge0 /=; split => //.
case=> [r| |//].
* rewrite lte_fin/= posnum_max pos_lt_maxl /= => /andP[MPx MQx]; split.
by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx)// real_ler_normr ?lexx.
by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx.
* by move=> _; split; [apply/gtMP | apply/gtMQ].
+ by exists M; split => // ? /gtM /sPQ.
* rewrite lee_fin /= posnum_max pos_le_maxl /= => /andP[MPx MQx]; split.
by apply/geMP; rewrite lee_fin (le_trans _ MPx)// real_ler_normr ?lexx.
by apply/geMQ; rewrite lee_fin (le_trans _ MQx)// real_ler_normr ?lexx.
* by move=> _; split; [apply/geMP | apply/geMQ].
+ by exists M; split => // ? /geM /sPQ.
- apply Build_ProperFilter.
+ move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0.
+ split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
by apply: ltMP; rewrite lee_fin ger_addl oppr_le0.
+ split=> /= [|P Q [MP [MPr leMP]] [MQ [MQr leMQ]] |P Q sPQ [M [Mr leM]]].
* by exists 0%R; rewrite real0.
* have [MP0|MP0] := eqVneq MP 0%R.
have [MQ0|MQ0] := eqVneq MQ 0%R.
by exists 0%R; rewrite real0; split => // x x0; split;
[apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
[apply/leMP; rewrite MP0 | apply/leMQ; rewrite MQ0].
exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ.
split.
by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
by apply leMP; rewrite (le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
apply leMQ; rewrite (le_trans xMQ) // lee_fin ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
* have [MQ0|MQ0] := eqVneq MQ 0%R.
exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx.
split.
apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
apply leMP; rewrite (le_trans MPx) // lee_fin ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
by apply leMQ; rewrite (le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
rewrite realN realE /= posnum_ge0 /=; split => //.
case=> [r|//|].
- rewrite lte_fin ltr_oppr posnum_max pos_lt_maxl => /andP[].
rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN.
- rewrite lee_fin ler_oppr posnum_max pos_le_maxl => /andP[].
rewrite ler_oppr => MPx; rewrite ler_oppr => MQx; split.
apply/leMP; rewrite lee_fin (le_trans MPx) //= ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= ler_oppl -normrN.
apply/leMQ; rewrite lee_fin (le_trans MQx) //= ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
- by move=> _; split; [apply/ltMP | apply/ltMQ].
* by exists M; split => // x /ltM /sPQ.
- by move=> _; split; [apply/leMP | apply/leMQ].
* by exists M; split => // x /leM /sPQ.
Qed.
Typeclasses Opaque ereal_dnbhs.

Expand Down Expand Up @@ -2562,30 +2578,30 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym.
- exists (M + 1)%R; split; first by rewrite realD // real1.
move=> -[x| _ |] //=.
rewrite lte_fin => M'x /=.
rewrite lee_fin => M'x /=.
apply/nbhs_ballP; exists 1%R => //= y x1y.
apply MA; rewrite lte_fin.
rewrite addrC -ltr_subr_addl in M'x.
rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
apply MA; rewrite lee_fin.
rewrite addrC -ler_subr_addl in M'x.
rewrite (le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
rewrite ltr_subr_addr in M'x.
rewrite ler_subr_addr in M'x.
rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //.
by rewrite /Order.comparable (ltW M'x) orbT.
by rewrite /Order.comparable M'x orbT.
by rewrite comparabler0 realD // real1.
by rewrite num_real. (* where we really use realFieldType *)
by exists M.
- exists (M - 1)%R; split; first by rewrite realB // real1.
move=> -[x| _ |] //=.
rewrite lte_fin => M'x /=.
rewrite lee_fin => M'x /=.
apply/nbhs_ballP; exists 1%R => //= y x1y.
apply MA; rewrite lte_fin.
rewrite ltr_subr_addl in M'x.
rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl.
apply MA; rewrite lee_fin.
rewrite ler_subr_addl in M'x.
rewrite (le_trans _ M'x) // addrC -ler_subl_addl.
rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
by rewrite num_real. (* where we really use realFieldType *)
rewrite addrC -ltr_subr_addr in M'x.
rewrite addrC -ler_subr_addr in M'x.
rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //.
by rewrite /Order.comparable (ltW M'x).
by rewrite /Order.comparable M'x.
by rewrite comparabler0 realB // real1.
by exists M.
Qed.
Expand Down Expand Up @@ -2615,19 +2631,19 @@ case: x => [r /=| |].
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (-%E @` S).
exists (- M)%R; rewrite realN Mreal; split => // x Mx.
by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK].
by exists (- x); [apply MS; rewrite lee_oppl | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (- x); [exists x | rewrite oppeK].
exists (- M)%R; rewrite realN; split => // y yM.
exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK].
exists (- y); by [apply Mx; rewrite lee_oppr|rewrite oppeK].
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (-%E @` S).
exists (- M)%R; rewrite realN Mreal; split => // x Mx.
by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK].
by exists (- x); [apply MS; rewrite lee_oppr | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (- x); [exists x | rewrite oppeK].
exists (- M)%R; rewrite realN; split => // y yM.
exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK].
exists (- y); by [apply Mx; rewrite lee_oppl|rewrite oppeK].
Qed.

Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
Expand Down Expand Up @@ -2990,12 +3006,15 @@ Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
ereal_ball +oo e%:num `<=` A -> nbhs +oo A.
Proof.
move=> e1 ooeA.
exists (fine (expand (1 - e%:num)%R)); rewrite num_real; split => //.
case => [r | | //].
- rewrite fine_expand; last first.
by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0.
by move=> ?; exact/ooeA/expand_ereal_ball_pinfty.
- by move=> _; exact/ooeA/ereal_ball_center.
exists (fine (expand (1 - e%:num / 2)%R)); rewrite num_real; split => //.
have e21 : (`|1 - e%:num / 2| < 1)%R.
rewrite ger0_norm; first by rewrite ltr_subl_addl ltr_addr.
by rewrite subr_ge0 ler_pdivr_mulr// mul1r (le_trans e1)// ler1n.
case => [r | _ | //]; last exact/ooeA/ereal_ball_center.
rewrite fine_expand // => er; apply/ooeA/expand_ereal_ball_pinfty => //.
rewrite (lt_le_trans _ er)// lt_expand ?inE; last exact/ltW.
by rewrite ler_lt_sub// ltr_pdivr_mulr// ltr_pmulr// ltr1n.
by rewrite ger0_norm ?subr_ge0// ler_subl_addl addrC -ler_subl_addl subrr.
Qed.

Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
Expand Down Expand Up @@ -3261,12 +3280,12 @@ rewrite predeq2E => x A; split.
by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
case=> [r| |]/=.
* rewrite /ereal_ball [_ +oo]/= => rM1.
apply: MA; rewrite lte_fin.
apply: MA; rewrite lee_fin.
rewrite ger0_norm in rM1; last first.
by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm.
rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr in rM1.
rewrite subr_gt0 in rM1.
by rewrite -lte_fin -lt_contract.
by rewrite -lee_fin -le_contract ltW.
* by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
* rewrite /ereal_ball /= opprK => h {MA}.
exfalso.
Expand All @@ -3281,12 +3300,12 @@ rewrite predeq2E => x A; split.
case=> [r| |].
* rewrite /ereal_ball => /= rM1.
apply MA.
rewrite lte_fin.
rewrite lee_fin.
rewrite ler0_norm in rM1; last first.
rewrite ler_subl_addl addr0 ltW //.
by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
rewrite opprB opprK -ltr_subl_addl addrK in rM1.
by rewrite -lte_fin -lt_contract.
by rewrite -lee_fin -le_contract ltW.
* rewrite /ereal_ball /= -opprD normrN => h {MA}.
exfalso.
move: h; apply/negP.
Expand Down Expand Up @@ -3383,14 +3402,14 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat.
by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
exists N.+1 => // n ltNn; apply: dP.
have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
have /le_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor.
by rewrite -(@natrD R N 1) ler_nat addn1.
have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltr_oppl.
have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
exists N.+1 => // n ltNn; apply: dP; rewrite lee_fin ler_oppl.
have /le_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor.
by rewrite -(@natrD R N 1) ler_nat addn1.
have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
by rewrite Znat_def floor_ge0.
Expand Down
27 changes: 16 additions & 11 deletions theories/normedtype.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2207,10 +2207,10 @@ move=> [x| |] /=.
exact: (cvg_comp (@scaler_continuous _ _ _ _)).
- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0).
by move=> x rux; apply uA; move: rux; rewrite mulEFin lte_pdivr_mull.
by move=> x rux; apply uA; move: rux; rewrite mulEFin lee_pdivr_mull.
- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0).
by move=> x xru; apply uA; move: xru; rewrite mulEFin lte_pdivl_mull.
by move=> x xru; apply uA; move: xru; rewrite mulEFin lee_pdivl_mull.
Grab Existential Variables. all: end_near. Qed.

End mule_continuous.
Expand Down Expand Up @@ -3597,24 +3597,28 @@ case: x => [x|//|] xy; first exact: open_ereal_lt.
- case: y => [y||//] /= in xy *; last by exists 0%R.
by exists y; rewrite num_real; split => //= x ?.
- case: y => [y||//] /= in xy *.
+ by exists y; rewrite num_real; split => //= x ?.
+ exists 0%R; rewrite real0; split => // x.
by move/lt_le_trans; apply; rewrite lee_pinfty.
+ exists (y - 1)%R; rewrite num_real; split => //= x /le_lt_trans; apply.
by rewrite lte_fin ltr_subl_addr ltr_addl.
+ exists 0%R; rewrite real0; split => // x /le_lt_trans; apply.
by rewrite lte_pinfty.
Qed.

Lemma open_ereal_gt' x y : y < x -> ereal_nbhs x (fun u => y < u).
Proof.
case: x => [x||] //=; do ?[exact: open_ereal_gt];
case: y => [y||] //=; do ?by exists 0; rewrite real0.
- by exists y; rewrite num_real.
- exists (y + 1)%R; rewrite num_real; split => // x /lt_le_trans; apply.
by rewrite lte_fin ltr_addl.
- move=> _; exists 0%R; rewrite real0; split => // x.
by apply/le_lt_trans; rewrite lee_ninfty.
by apply/lt_le_trans; rewrite lte_ninfty.
Qed.

Let open_ereal_lt_real r : open (fun x => x < r%:E).
Proof.
case => [? | // | ?]; [rewrite lte_fin => xy | by exists r].
by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
case => [? | // | ?]; [rewrite lte_fin => xy | exists (r - 1)%R].
by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
rewrite num_real; split => // x /le_lt_trans; apply.
by rewrite lte_fin ltr_subl_addr ltr_addl.
Qed.

Lemma open_ereal_lt_ereal x : open [set y | y < x].
Expand All @@ -3631,8 +3635,9 @@ Qed.

Let open_ereal_gt_real r : open (fun x => r%:E < x).
Proof.
case => [? | ? | //]; [rewrite lte_fin => xy | by exists r].
by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
case => [? | ? | //]; [rewrite lte_fin => xy | exists (r + 1)%R].
by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
by rewrite num_real; split=> // x /lt_le_trans; apply; rewrite lte_fin ltr_addl.
Qed.

Lemma open_ereal_gt_ereal x : open [set y | x < y].
Expand Down
14 changes: 12 additions & 2 deletions theories/posnum.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,12 +134,22 @@ Proof. by rewrite lt_geF. Qed.
Lemma posnum_lt0 x : (x%:num < 0 :> R) = false.
Proof. by rewrite lt_gtF. Qed.

Lemma pos_lt_maxl a x y : Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a).
Lemma pos_lt_maxl a x y :
Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a).
Proof. by rewrite comparable_lt_maxl ?real_comparable. Qed.

Lemma pos_lt_minr (a : R) x y : a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
Lemma pos_le_maxl a x y :
Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a).
Proof. by rewrite comparable_le_maxl ?real_comparable. Qed.

Lemma pos_lt_minr a x y :
a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
Proof. by rewrite comparable_lt_minr ?real_comparable. Qed.

Lemma pos_le_minr (a : R) x y :
a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num).
Proof. by rewrite comparable_le_minr ?real_comparable. Qed.

Lemma min_pos_gt0 x y : 0 < Num.min x%:num y%:num.
Proof. by rewrite -posnum_min !posnum_gt0. Qed.
Canonical minr_posnum x y := PosNum (@min_pos_gt0 x y).
Expand Down
Loading

0 comments on commit 5a4a8ea

Please sign in to comment.