Monotonicity lemmas for norms

CHANGELOG_UNRELEASED.md

@@ -33,6 +33,8 @@
     `wlength_sigma_sub_additive`, `wlength_sigma_finite`
   + measure instance of `hlength`
   + definition `lebesgue_stieltjes_measure`
+- in `mathcomp_extra.v`
+  + lemmas `ge0_ler_normr`, `gt0_ler_normr`, `le0_ger_normr` and `lt0_ger_normr`
 
 ### Changed
 

classical/mathcomp_extra.v

@@ -1442,3 +1442,31 @@ Arguments le_bigmax_seq {d T} x {I r} i0 P.
 (* NB: PR 1079 to MathComp in progress *)
 Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
 Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed.
+
+(* the following appears in MathComp 2.1.0 and MathComp 1.18.0 *)
+Section normr.
+Variable R : realDomainType.
+
+Definition Rnpos : qualifier 0 R := [qualify x : R | x <= 0].
+Lemma nposrE x : (x \is Rnpos) = (x <= 0). Proof. by []. Qed.
+
+Lemma ger0_le_norm :
+  {in Num.nneg &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
+Proof. by move=> x y; rewrite !nnegrE => x0 y0; rewrite !ger0_norm. Qed.
+
+Lemma gtr0_le_norm :
+  {in Num.pos &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
+Proof. by move=> x y; rewrite !posrE => /ltW x0 /ltW y0; exact: ger0_le_norm. Qed.
+
+Lemma ler0_ge_norm :
+  {in Rnpos &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
+Proof.
+move=> x y; rewrite !nposrE => x0 y0.
+by rewrite !ler0_norm// -subr_ge0 opprK addrC subr_ge0.
+Qed.
+
+Lemma ltr0_ge_norm :
+  {in Num.neg &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
+Proof. by move=> x y; rewrite !negrE => /ltW x0 /ltW y0; exact: ler0_ge_norm. Qed.
+
+End normr.