Module mathcomp.classical.unstable

From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
From mathcomp Require Import archimedean interval.

# MathComp extra This files contains lemmas that should eventually be backported to mathcomp. These lemmas may change before being backported to mathcomp, don't use anything in this file outside of Analysis. For this same reason, nothing in this file should be mentionned in the changelog. Once a result is backported to mathcomp, please move it to mathcomp_extra.v and mention it in the changelog. ``` swap x := (x.2, x.1) map_pair f x := (f x.1, f x.2) monotonic A f := {in A &, {homo f : x y / x <= y}} \/ {in A &, {homo f : x y /~ x <= y}} strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/ {in A &, {homo f : x y /~ x < y}} sigT_fun f := lifts a family of functions f into a function on the dependent sum prodA x := sends (X * Y) * Z to X * (Y * Z) prodAr x := sends X * (Y * Z) to (X * Y) * Z ```

Attributes warn(note="The unstable.v file should only be used inside analysis.",
  cats="internal-analysis").

Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Section IntervalNumDomain.
Variable : numDomainType.
Implicit Types x : R.

Lemma ( : R) :
  (- x \in Interval (BInfty _ ba) (BSide bb xb)) =
  (x \in Interval (BSide (~~ bb) (- xb)) (BInfty _ (~~ ba))).

Proof.

by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNl andbC.
Qed.

Lemma ( : R) :
(- x \in Interval (BSide ba xa) (BInfty _ bb)) =
(x \in Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- xa))).

Proof.

by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNr negbK andbC.
Qed.

End IntervalNumDomain.

Lemma ( : Type) ( : seq I) ( : {pred I}) ( : I -> nat) ( : I)
    ( : seq I) :
  all (coprime (F a)) [seq F i | <- [seq <- l | P i]] ->
  coprime (F a) (\prod_( <- l | P j) F j).

Proof.

elim: l => /= [_|h t ih]; first by rewrite big_nil coprimen1.
rewrite big_cons; case: ifPn => // Ph.
rewrite map_cons => /= /andP[FaFh FatP].
by rewrite coprimeMr FaFh/= ih.
Qed.

Lemma ( : eqType) ( : seq I) ( : {pred I}) ( : I -> nat)
    ( : nat) :
  pairwise coprime [seq F i | <- [seq <- r | P i]] ->
  reflect (forall , i \in r -> P i -> F i %| n)
          (\prod_( <- r | P i) F i %| n).

Proof.

elim: r => /= [_|a l HI].
  by rewrite big_nil dvd1n; apply: ReflectT => i; rewrite in_nil.
rewrite big_cons; case: ifP => [Pa|nPa]; last first.
  move/HI/equivP; apply; split=> [Fidvdn i|Fidvdn i il].
    by rewrite in_cons => /predU1P[->|]; [rewrite nPa|exact: Fidvdn].
  by apply: Fidvdn; rewrite in_cons il orbT.
rewrite map_cons pairwise_cons => /andP[allcoprimea pairwisecoprime].
rewrite Gauss_dvd; last exact: coprime_prodr.
apply: (equivP (andPP idP (HI pairwisecoprime))).
split=> [[Fadvdn Fidvdn] i|Fidvdn].
  by rewrite in_cons => /predU1P[->//|]; exact: Fidvdn.
split=> [|i il].
  by apply: Fidvdn => //; exact: mem_head.
by apply: Fidvdn; rewrite in_cons il orbT.
Qed.

Lemma ( : eqType) ( : seq I) ( : {pred I}) ( : I -> nat)
( : nat) :
((\prod_( <- r | P i) F i) ^ n = \prod_( <- r | P i) (F i) ^ n)%N.

Proof.

elim: r => [|a l]; first by rewrite !big_nil exp1n.
by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn.
Qed.

Lemma ( : nat) : (n <= x)%N -> (m <= y)%N ->
(\prod_(m <= < y) i * \prod_(n <= < x) i <= \prod_(n + m <= < x + y) i)%N.

Proof.

move=> nx my; rewrite big_addn -addnBA//.
rewrite [in leqRHS]/index_iota -addnBAC// iotaD big_cat/=.
rewrite mulnC leq_mul//.
by apply: leq_prod; move=> i _; rewrite leq_addr.
rewrite subnKC//.
rewrite -[in leqLHS](add0n m) big_addn.
rewrite [in leqRHS](_ : y - m = ((y - m + x) - x))%N; last first.
by rewrite -addnBA// subnn addn0.
rewrite -[X in iota X _](add0n x) big_addn -addnBA// subnn addn0.
by apply: leq_prod => i _; rewrite leq_add2r leq_addr.
Qed.

Lemma ( : nat) : (n <= x) %N -> (m <= y)%N ->
(x`! * y`! * ((n + m).+1)`! <= n`! * m`! * ((x + y).+1)`!)%N.

Proof.

move=> nx my.
rewrite (fact_split nx) -!mulnA leq_mul2l; apply/orP; right.
rewrite (fact_split my) mulnCA -!mulnA leq_mul2l; apply/orP; right.
rewrite [leqRHS](_ : _ =
(n + m).+1`! * \prod_((n + m).+2 <= < (x + y).+2) i)%N; last first.
by rewrite -fact_split// ltnS leq_add.
rewrite mulnA mulnC leq_mul2l; apply/orP; right.
do 2 rewrite -addSn -addnS.
exact: leq_Mprod_prodD.
Qed.

Section max_min.
Variable : realFieldType.

Let : 2%:R != 0 :> R

Proof.

by rewrite pnatr_eq0. Qed.

Lemma ( : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.

Proof.

apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
by rewrite addrCA addrK.
by rewrite (addrC (x + y)) subrKA.
Qed.

Lemma ( : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.

Proof.

apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *)
by rewrite -mulrDl addrCA addrK mulrDl -splitr.
Qed.

End max_min.

Notation := (ltac:(done)).

Section bigmax_seq.
Context { : orderType d} { : T} { : eqType}.
Variables ( : seq I) ( : I) ( : pred I).

Lemma :
i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_( <- r | P i) F i)%O.

Proof.

move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx.
by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih].
Qed.

Lemma ( : T) ( : I -> T) :
i0 \in r -> P i0 -> (m <= F i0)%O ->
(m <= \big[Order.max/x]_( <- r | P i) F i)%O.

Proof.

by move=> i0r Pi0 ?; apply: le_trans (le_bigmax_seq _ _ _). Qed.

End bigmax_seq.
Arguments le_bigmax_seq {d T} x {I r} i0 P.

Lemma : exists , (2 ^ n <= m.+1 < 2 ^ n.+1)%N.

Proof.

elim: m => [|m [n /andP[h1 h2]]]; first by exists O.
have [m2n|nm2] := ltnP m.+2 (2 ^ n.+1)%N.
by exists n; rewrite m2n andbT (leq_trans h1).
exists n.+1; rewrite nm2/= -addn1.
rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
Qed.

Definition ( : porderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :=
  {in A &, nondecreasing f} \/ {in A &, {homo f : /~ (x <= y)%O}}.

Definition ( : porderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :=
  {in A &, {homo f : / (x < y)%O}} \/ {in A &, {homo f : /~ (x < y)%O}}.

Lemma ( : orderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :
  strict_monotonic A f -> monotonic A f.

Proof.

by move=> [/le_mono_in/monoW_in|/le_nmono_in/monoW_in]; [left|right].
Qed.

Lemma : {mono f : / (m <= n)%N} -> forall , (n <= f n)%N.

Proof.

move=> fincr; elim=> [//| n HR]; rewrite (leq_ltn_trans HR)//.
by rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle.
Qed.

Section path_lt.
Context { : orderType d}.
Implicit Types (a b c : T) (s : seq T).

Lemma ( : pred T) :
P a -> P (last a [seq <- s | P x]).

Proof.

by elim: s a => //= t1 t2 ih a Pa; case: ifPn => //= Pt1; exact: ih.
Qed.

Lemma : path <%O a s -> [seq <- s | (x < a)%O] = [::].

Proof.

move=> /lt_path_min/allP sa; rewrite -(filter_pred0 s).
apply: eq_in_filter => x xs.
by apply/negbTE; have := sa _ xs; rewrite ltNge; apply: contra => /ltW.
Qed.

Lemma : path <%O a s -> [seq <- s | (a < x)%O] = s.

Proof.

move=> /lt_path_min/allP sa; rewrite -[RHS](filter_predT s).
by apply: eq_in_filter => x xs; exact: sa.
Qed.

Lemma : (a < b)%O -> path <%O b s -> path <%O a s.

Proof.

by elim: s b => // h t ih b /= ab /andP[bh ->]; rewrite andbT (lt_trans ab).
Qed.

Lemma :
(a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b ->
last c [seq <- s | (c < x)%O] = b.

Proof.

elim/last_ind : s a b c => /= [|h t ih a b c ac cb].
move=> a b c ac cb _ ab.
by apply/eqP; rewrite eq_le (ltW cb) -ab (ltW ac).
rewrite rcons_path => /andP[ah ht]; rewrite last_rcons => tb.
by rewrite filter_rcons tb cb last_rcons.
Qed.

Lemma : path <%O a s -> (a <= last a s)%O.

Proof.

elim: s a => // a [_ c /andP[/ltW//]|b t ih i/= /and3P[ia ab bt]] /=.
have /= := ih a; rewrite ab bt => /(_ erefl).
by apply: le_trans; exact/ltW.
Qed.

End path_lt.
Arguments last_filterP {d T a} P s.

Inductive := of T.

Reserved Notation "`1- r" (format "`1- r", at level 2).
Reserved Notation "f \^-1" (at level 35, format "f \^-1").

Lemma ( : choiceType) ( : {fset X})
( : X -> nat) : A != fset0 ->
(exists , i \in A /\ forall , j \in A -> f j <= f i)%nat.

Proof.

move=> /fset0Pn[x Ax].
have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT.
exists (val y); split; first exact: valP.
by move=> z Az; have := mf [` Az]%fset.
Qed.

Lemma ( : nat -> nat) :
(exists , i <= n /\ forall , j <= n -> f j <= f i)%N.

Proof.

have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT.
by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn).
Qed.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

Reserved Notation "`1- x" (format "`1- x", at level 2).

Lemma ( : Type) ( : finType) ( : seq I) ( : {pred I})
( : I -> {set T}) :
(#|\bigcup_( <- r | P i) F i| <= \sum_( <- r | P i) #|F i|)%N.

Proof.

elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0.
by rewrite (leq_trans (leq_card_setU _ _))// leq_add.
Qed.

Definition { : pzRingType} ( : R) : R := 1 - r.
#[deprecated(since="mathcomp-analysis 1.15.0")]
Notation := (onem r) : ring_scope.

Reserved Notation "p '.~'" (format "p .~", at level 1).
Notation := (onem p) : ring_scope.

Section onem_ring.
Context { : pzRingType}.
Implicit Type r : R.

Lemma : 0.~ = 1 :> R

Proof.

by rewrite /onem subr0. Qed.

Lemma : 1.~ = 0 :> R

Proof.

by rewrite /onem subrr. Qed.

Lemma : (r.~).~ = r

Proof.

exact: subKr. Qed.

Lemma : r + r.~ = 1

Proof.

by rewrite /onem addrC subrK. Qed.

Lemma : (r + s).~ = r.~ - s.

Proof.

by rewrite /onem opprD addrA. Qed.

Lemma : s * r.~ = s - s * r.

Proof.

by rewrite /onem mulrBr mulr1. Qed.

Lemma : (r * s).~ = r.~ + s.~ - r.~ * s.~.

Proof.

by rewrite /onem mulrBl 2!mulrBr !mul1r mulr1 addrKA opprK subrKA. Qed.

End onem_ring.

Section onem_order.
Variable : numDomainType.
Implicit Types r : R.

Lemma : r < 1 -> 0 < r.~

Proof.

by rewrite subr_gt0. Qed.

Lemma : r <= 1 -> 0 <= r.~.

Proof.

by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.

Lemma : 0 <= r -> r.~ <= 1.

Proof.

by rewrite lerBlDr lerDl. Qed.

Lemma : 0 < r -> r.~ < 1.

Proof.

by rewrite ltrBlDr ltrDl. Qed.

Lemma : 0 <= r -> r <= 1 -> 0 <= (r ^+ n).~.

Proof.

by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed.

Lemma : 0 < r -> (r ^+ n).~ < 1.

Proof.

by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.

End onem_order.

Lemma { : realDomainType} ( : R) :
(0 <= x <= 1 -> `| x.~ | <= 1)%R.

Proof.

move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split.
by rewrite lerBrDl lerBlDr (le_trans x1)// lerDl.
by rewrite lerBlDr lerDl.
Qed.

Lemma ( : numFieldType) ( : F) : x != 0 -> x^-1.~ = (x - 1) / x.

Proof.

by move=> ?; rewrite mulrDl divff// mulN1r. Qed.

Lemma ( : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.

Proof.

by case: a => //= n _; case: b. Qed.

Lemma ( : numFieldType) ( : R) :
reflect (forall , z > y -> x <= z) (x <= y).

Proof.

apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
by rewrite -subr_gt0 => /xy; rewrite addrC addrNK.
by apply: xz; rewrite -[ltLHS]addr0 ler_ltD.
Qed.

Lemma ( : numFieldType) ( : R) :
reflect (forall , z < x -> z <= y) (x <= y).

Proof.

apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
by rewrite -subr_gt0 => /xy; rewrite addrCA -[leLHS]addr0 lerD2l subr_ge0.
by rewrite -lerBlDr xz// -[ltRHS]subr0 ler_ltB.
Qed.

Definition ( : unitRingType) ( : T -> R) := (f x)^-1%R.
Notation := (inv_fun f) : ring_scope.
Arguments inv_fun {T R} _ _ /.

Definition ( : porderType d) ( : bool) ( : itv_bound T) :=
if x is BSide c' _ then c == c' else false.

Lemma [ : numDomainType] [ : R] ( : R) :
x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).

Proof.

by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.

Definition { : Type} ( : T1 * T2) := (x.2, x.1).

Section reassociate_products.
Context { : Type}.

Definition ( : (X * Y) * Z) : X * (Y * Z) :=
(xyz.1.1, (xyz.1.2, xyz.2)).

Definition ( : X * (Y * Z)) : (X * Y) * Z :=
((xyz.1, xyz.2.1), xyz.2.2).

Lemma : cancel prodA prodAr.

Proof.

by case; case. Qed.

Lemma : cancel prodAr prodA.

Proof.

by case => ? []. Qed.

End reassociate_products.

Lemma { : Type} : cancel (@swap T1 T2) (@swap T2 T1).

Proof.

by case=> ? ?. Qed.

Definition { : Type} ( : S -> U) ( : (S * S)) : (U * U) :=
(f x.1, f x.2).

Section order_min.
Variables ( : Order.disp_t) ( : orderType d).

Lemma ( : T) : (Order.min x z < Order.min y z)%O -> (x < y)%O.

Proof.

rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
- by move=> /lt_le_trans; apply; rewrite leNgt.
- by rewrite ltNge (ltW yz).
Qed.

End order_min.

Section bijection_forall.

Lemma ( : A -> B) ( : B -> Prop) :
bijective f -> (forall , P y) <-> (forall , P (f x)).

Proof.

by case; rewrite /cancel => g _ cangf; split => // => ? y; rewrite -(cangf y).
Qed.

End bijection_forall.

Lemma ( : Type) ( : mem_pred T) ( : T -> Prop) :
{in p, forall , P x /\ Q x} <->
{in p, forall , P x} /\ {in p, forall , Q x}.

Proof.

split=> [cnd|[cnd1 cnd2] x xin]; first by split=> x xin; case: (cnd x xin).
by split; [apply: cnd1 | apply: cnd2].
Qed.

Lemma ( : porderType d) ( : T) ( : T -> T) :
{in `[a, b] &, {mono f : / (x <= y)%O}} ->
{homo f : / x \in `[a, b] >-> x \in `[f a, f b]}.

Proof.

move=> fle x xab; have leab : (a <= b)%O by rewrite (itvP xab).
by rewrite in_itv/= !fle ?(itvP xab).
Qed.

Lemma ( : porderType d) ( : T) ( : T -> T) :
{in `[a, b] &, {mono f : /~ (x <= y)%O}} ->
{homo f : / x \in `[a, b] >-> x \in `[f b, f a]}.

Proof.

move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab).
by rewrite in_itv/= !fge ?(itvP xab).
Qed.

Definition { : Type} { : I -> Type} { : Type}
  ( : forall , X i -> T) ( : { & X i}) : T :=
  (f (projT1 x) (projT2 x)).

Section FsetPartitions.
Variables : choiceType.
Implicit Types (x y z : T) (A B D X : {fset T}) (P Q : {fset {fset T}}).
Implicit Types (J : pred I) (F : I -> {fset T}).

Variables ( : Type) ( : R) ( : Monoid.com_law idx).
Let :=
  (\big[op/idx]_( <- P) \big[op/idx]_( <- A | K x) E x)%fset.
Let := (\big[op/idx]_( <- P) \big[op/idx]_( <- A) E x)%fset.

Lemma ( : T -> R) ( : I -> {fset T})
  ( : {fset I}) :
  (forall , i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset ->
  \big[op/idx]_( <- \big[fsetU/fset0]_( <- K) (F x)) f i =
  \big[op/idx]_( <- K) (\big[op/idx]_( <- F k) f i).

Proof.

move=> disjF; pose P := [fset F i | in K & F i != fset0]%fset.
have trivP : trivIfset P.
  apply/trivIfsetP => _ _ /imfsetP[i iK ->] /imfsetP[j jK ->] neqFij.
  move: iK; rewrite !inE/= => /andP[iK Fi0].
  move: jK; rewrite !inE/= => /andP[jK Fj0].
  by apply: (disjF _ _ iK jK); apply: contraNneq neqFij => ->.
have -> : (\bigcup_( <- K) F i)%fset = fcover P.
  apply/esym; rewrite /P fcover_imfset big_mkcond /=; apply eq_bigr => i _.
  by case: ifPn => // /negPn/eqP.
rewrite big_trivIfset // /rhs big_imfset => [|i j iK /andP[jK notFj0] eqFij] /=.
  rewrite big_filter big_mkcond; apply eq_bigr => i _.
  by case: ifPn => // /negPn /eqP ->; rewrite big_seq_fset0.
move: iK; rewrite !inE/= => /andP[iK Fi0].
by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid.
Qed.

End FsetPartitions.

Lemma { : realDomainType} ( : seq R) :
(forall , x \in s -> 0 <= x <= 1)%R -> (\prod_( <- s) j <= 1)%R.

Proof.

elim: s => [_ | y s ih xs01]; rewrite ?big_nil// big_cons.
have /andP[y0 y1] : (0 <= y <= 1)%R by rewrite xs01// mem_head.
rewrite mulr_ile1 ?andbT//.
rewrite big_seq prodr_ge0// => x xs.
by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[].
by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
Qed.

Lemma ( : seq T) : (size (filter P r) > 0)%N = (has P r).

Proof.

by elim: r => //= x r; case: ifP. Qed.

Lemma [ : numDomainType] [ : Type] ( : seq I)
    [ : pred I] [ : I -> R] :
  has P r ->
  (forall : I, P i -> F i < G i) ->
  \sum_( <- r | P i) F i < \sum_( <- r | P i) G i.

Proof.

rewrite -big_filter -[ltRHS]big_filter -size_filter_gt0.
case: filter (filter_all P r) => //= x {}r /andP[Px Pr] _ ltFG.
rewrite !big_cons ltr_leD// ?ltFG// -(all_filterP Pr) !big_filter.
by rewrite ler_sum => // i Pi; rewrite ltW ?ltFG.
Qed.

Lemma [ : numDomainType] [ : nat] [ : nat -> R] :
(m < n)%N -> (forall : nat, (m <= i < n)%N -> F i < G i) ->
\sum_(m <= < n) F i < \sum_(m <= < n) G i.

Proof.

move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//.
by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn.
Qed.

Lemma ( : Type) ( : A -> Prop) :
(forall , P x <-> P' x) ->
(exists2 , P x & Q x) <-> (exists2 , P' x & Q x).

Proof.

by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
Qed.

Lemma ( : Type) ( : A -> Prop) :
(forall , Q x <-> Q' x) ->
(exists2 , P x & Q x) <-> (exists2 , P x & Q' x).

Proof.

by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP.
Qed.

Declare Scope signature_scope.
Delimit Scope signature_scope with signature.

Import -(notations) Morphisms.
Arguments Proper {A}%_type R%_signature m.
Arguments respectful {A B}%_type (R R')%_signature _ _.

Module .

Notation := (@respectful _ _ (R%signature) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Notation := (@respectful _ _ (R%signature) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Notation := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Export -(notations) Morphisms.
End ProperNotations.

Lemma { : rcfType} : {in Num.nneg, cancel (@Num.sqrt K) (fun => x ^+ 2)}.

Proof.

by move=> r r0; rewrite sqr_sqrtr. Qed.

Lemma { : archiNumDomainType} ( : R) : `|x| < (Num.bound x)%:R.

Proof.

by rewrite /Num.bound -[in ltRHS]normr_id archi_boundP. Qed.

Lemma { : archiNumDomainType} ( : R) :
x \is Num.real -> x < (Num.bound x)%:R.

Proof.

by move=> /real_ler_norm /le_lt_trans -> //; apply: ltr_norm_bound. Qed.

Lemma { : archiNumDomainType} ( : R) :
x \is Num.real -> - x < (Num.bound x)%:R.

Proof.

by rewrite /Num.bound -realN -normrN; exact: real_ltr_bound. Qed.

Lemma { : archiRealDomainType} ( : R) : x < (Num.bound x)%:R.

Proof.

exact: real_ltr_bound. Qed.

Lemma { : archiRealDomainType} ( : R) : - x < (Num.bound x)%:R.

Proof.

exact: real_ltrNbound. Qed.

Files

Module mathcomp.classical.unstable