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 R : numDomainType.
Implicit Types x : R.

Lemma oppr_itvNy ba bb (xa xb x : 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 oppr_itvy ba bb (xa x : 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 coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I)
    (l : seq I) :
  all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] ->
  coprime (F a) (\prod_(j <- 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 Gauss_dvd_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
    (n : nat) :
  pairwise coprime [seq F i | i <- [seq i <- r | P i]] ->
  reflect (forall i, i \in r -> P i -> F i %| n)
          (\prod_(i <- 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 expn_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
(n : nat) :
((\prod_(i <- r | P i) F i) ^ n = \prod_(i <- 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 leq_Mprod_prodD (x y n m : nat) : (n <= x)%N -> (m <= y)%N ->
(\prod_(m <= i < y) i * \prod_(n <= i < x) i <= \prod_(n + m <= i < 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 leq_fact2 (x y n m : 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 <= i < (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 R : realFieldType.

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

Proof.

by rewrite pnatr_eq0. Qed.

Lemma maxr_absE (x y : 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 minr_absE (x y : 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 trivial := (ltac:(done)).

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

Lemma le_bigmax_seq F :
i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- 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 bigmax_sup_seq (m : T) (F : I -> T) :
i0 \in r -> P i0 -> (m <= F i0)%O ->
(m <= \big[Order.max/x]_(i <- 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 leq_ltn_expn m : exists n, (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 d (T : porderType d) d' (T' : porderType d')
    (pT : predType T) (A : pT) (f : T -> T') :=
  {in A &, nondecreasing f} \/ {in A &, {homo f : x y /~ (x <= y)%O}}.

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

Lemma strict_monotonicW d (T : orderType d) d' (T' : porderType d')
    (pT : predType T) (A : pT) (f : 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_leq_infl f : {mono f : m n / (m <= n)%N} -> forall n, (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 d {T : orderType d}.
Implicit Types (a b c : T) (s : seq T).

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

Proof.

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

Lemma path_lt_filter0 a s : path <%O a s -> [seq x <- 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_lt_filterT a s : path <%O a s -> [seq x <- 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 path_lt_head a b s : (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 path_lt_last_filter a b c s :
(a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b ->
last c [seq x <- 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_lt_le_last a s : 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 boxed T := Box of T.

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

Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
(f : X -> nat) : A != fset0 ->
(exists i, i \in A /\ forall j, 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 image_nat_maximum n (f : nat -> nat) :
(exists i, i <= n /\ forall j, 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 card_big_setU (I : Type) (T : finType) (r : seq I) (P : {pred I})
(F : I -> {set T}) :
(#|\bigcup_(i <- r | P i) F i| <= \sum_(i <- 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 {R : pzRingType} (r : R) : R := 1 - r.
#[deprecated(since="mathcomp-analysis 1.15.0")]
Notation "`1- r" := (onem r) : ring_scope.

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

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

Lemma onem0 : 0.~ = 1 :> R

Proof.

by rewrite /onem subr0. Qed.

Lemma onem1 : 1.~ = 0 :> R

Proof.

by rewrite /onem subrr. Qed.

Lemma onemK r : (r.~).~ = r

Proof.

exact: subKr. Qed.

Lemma add_onemK r : r + r.~ = 1

Proof.

by rewrite /onem addrC subrK. Qed.

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

Proof.

by rewrite /onem opprD addrA. Qed.

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

Proof.

by rewrite /onem mulrBr mulr1. Qed.

Lemma onemM r s : (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 R : numDomainType.
Implicit Types r : R.

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

Proof.

by rewrite subr_gt0. Qed.

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

Proof.

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

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

Proof.

by rewrite lerBlDr lerDl. Qed.

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

Proof.

by rewrite ltrBlDr ltrDl. Qed.

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

Proof.

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

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

Proof.

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

End onem_order.

Lemma normr_onem {R : realDomainType} (x : 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 onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x.

Proof.

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

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

Proof.

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

Lemma ler_gtP (R : numFieldType) (x y : R) :
reflect (forall z, 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 ler_ltP (R : numFieldType) (x y : R) :
reflect (forall z, 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 T (R : unitRingType) (f : T -> R) x := (f x)^-1%R.
Notation "f \^-1" := (inv_fun f) : ring_scope.
Arguments inv_fun {T R} _ _ /.

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

Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : 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 {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).

Section reassociate_products.
Context {X Y Z : Type}.

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

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

Lemma prodAK : cancel prodA prodAr.

Proof.

by case; case. Qed.

Lemma prodArK : cancel prodAr prodA.

Proof.

by case => ? []. Qed.

End reassociate_products.

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

Proof.

by case=> ? ?. Qed.

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

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

Lemma lt_min_lt (x y z : 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 bij_forall A B (f : A -> B) (P : B -> Prop) :
bijective f -> (forall y, P y) <-> (forall x, P (f x)).

Proof.

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

End bijection_forall.

Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) :
{in p, forall x, P x /\ Q x} <->
{in p, forall x, P x} /\ {in p, forall x, 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 mem_inc_segment d (T : porderType d) (a b : T) (f : T -> T) :
{in `[a, b] &, {mono f : x y / (x <= y)%O}} ->
{homo f : x / 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 mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) :
{in `[a, b] &, {mono f : x y /~ (x <= y)%O}} ->
{homo f : x / 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 {I : Type} {X : I -> Type} {T : Type}
  (f : forall i, X i -> T) (x : {i & X i}) : T :=
  (f (projT1 x) (projT2 x)).

Section FsetPartitions.
Variables T I : 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 (R : Type) (idx : R) (op : Monoid.com_law idx).
Let rhs_cond P K E :=
  (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A | K x) E x)%fset.
Let rhs P E := (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A) E x)%fset.

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

Proof.

move=> disjF; pose P := [fset F i | 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_(i <- 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 prodr_ile1 {R : realDomainType} (s : seq R) :
(forall x, x \in s -> 0 <= x <= 1)%R -> (\prod_(j <- 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 size_filter_gt0 T P (r : seq T) : (size (filter P r) > 0)%N = (has P r).

Proof.

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

Lemma ltr_sum [R : numDomainType] [I : Type] (r : seq I)
    [P : pred I] [F G : I -> R] :
  has P r ->
  (forall i : I, P i -> F i < G i) ->
  \sum_(i <- r | P i) F i < \sum_(i <- 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 ltr_sum_nat [R : numDomainType] [m n : nat] [F G : nat -> R] :
(m < n)%N -> (forall i : nat, (m <= i < n)%N -> F i < G i) ->
\sum_(m <= i < n) F i < \sum_(m <= i < 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 eq_exists2l (A : Type) (P P' Q : A -> Prop) :
(forall x, P x <-> P' x) ->
(exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).

Proof.

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

Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) :
(forall x, Q x <-> Q' x) ->
(exists2 x, P x & Q x) <-> (exists2 x, 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 ProperNotations.

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

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

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

Export -(notations) Morphisms.
End ProperNotations.

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

Proof.

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

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

Proof.

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

Lemma real_ltr_bound {R : archiNumDomainType} (x : 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 real_ltrNbound {R : archiNumDomainType} (x : R) :
x \is Num.real -> - x < (Num.bound x)%:R.

Proof.

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

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

Proof.

exact: real_ltr_bound. Qed.

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

Proof.

exact: real_ltrNbound. Qed.

Files

Module mathcomp.classical.unstable