avoid name clash (#1814)

* avoid  name clash

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -173,6 +173,10 @@
 - in `charge.v`:
   + `induced` -> `induced_charge`
 
+- in `boolp.v`:
+  + `notP` -> `not_notP`
+  + `notE` -> `not_notE`
+
 ### Generalized
 
 - in `lebesgue_integral_under.v`:

classical/boolp.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
@@ -683,13 +683,18 @@ by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP.
 by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP.
 Qed.
 
-Lemma notP (P : Prop) : ~ ~ P <-> P.
+Lemma not_notP (P : Prop) : ~ ~ P <-> P.
 Proof. by split => [|p]; [exact: contrapT|exact]. Qed.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="Renamed to `not_notP`. Warning: a different `notP` is provided by `contra.v`.")]
+Notation notP := not_notP (only parsing).
 
-Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE notP. Qed.
+Lemma not_notE (P : Prop) : (~ ~ P) = P.
+Proof. by rewrite propeqE not_notP. Qed.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="Renamed to `not_notE`. Warning: a different `notE` is provided by `contra.v`.")]
+Notation notE := not_notE (only parsing).
 
 Lemma not_orE (P Q : Prop) : (~ (P \/ Q)) = (~ P /\ ~ Q).
-Proof. by rewrite -[_ /\ _]notE not_andE 2!notE. Qed.
+Proof. by rewrite -[_ /\ _]not_notE not_andE 2!not_notE. Qed.
 
 Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.
 Proof. by rewrite not_orE. Qed.
@@ -698,7 +703,7 @@ Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).
 Proof. by rewrite propeqE not_implyP. Qed.
 
 Lemma implyE (P Q : Prop) : (P -> Q) = (~ P \/ Q).
-Proof. by rewrite -[LHS]notE not_implyE propeqE not_andP notE. Qed.
+Proof. by rewrite -[LHS]not_notE not_implyE propeqE not_andP not_notE. Qed.
 
 Lemma orC : commutative or.
 Proof. by move=> /PropB[] /PropB[] => //; rewrite !orB. Qed.
@@ -1007,10 +1012,10 @@ Proof. by []. Qed.
 Section Inhabited.
 Variable (T : Type).
 
-Lemma inhabitedE: inhabited T = exists x : T, True.
+Lemma inhabitedE : inhabited T = exists x : T, True.
 Proof. by eqProp; case. Qed.
 
-Lemma inhabited_witness: inhabited T -> T.
+Lemma inhabited_witness : inhabited T -> T.
 Proof. by rewrite inhabitedE => /cid[]. Qed.
 
 End Inhabited.

classical/contra.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 From mathcomp Require Import boolp.
 
@@ -268,7 +268,9 @@ Lemma lax_notE {t nP} P : (~ nProp t nP P) = nP. Proof. by case: P. Qed.
 Lemma lax_notP {t nP P} : ~ nProp t nP P -> nP. Proof. by rewrite lax_notE. Qed.
 Definition lax_notI {t nP} P : nProp t nP P = (~ nP) := canRL notK (lax_notE P).
 
+#[warn(note="A different `notE` used to be provided by `boolp.v` before MathComp-Analysis 1.15.0.")]
 Definition notE {nP} P : (~ nProp false nP P) = nP := lax_notE P.
+#[warn(note="A different `notP` used to be provided by `boolp.v` before MathComp-Analysis 1.15.0.")]
 Definition notP {nP P} := MoveView (@lax_notP false nP P).
 
 Fact proper_nPropP nP P : (~ pnProp nP P) = nP. Proof. by case: P. Qed.

theories/normedtype_theory/normed_module.v

@@ -2300,7 +2300,7 @@ suff [p_idx [pUq Up]] : exists p_idx,
     by move/set_mem : pUq; exact: bigcup_ointsub_sub.
   exists (g p_idx).
   - rewrite /= => q' Uq' q'p.
-    apply/notP => /eqP/set0P[s [ps ts]].
+    apply/not_notP => /eqP/set0P[s [ps ts]].
     suff : ratr q' \in bigcup_ointsub U q by move/Up; rewrite leqNgt q'p.
     rewrite (@nondisjoint_bigcup_ointsub _ _ _ (g p_idx))//.
     rewrite (@nondisjoint_bigcup_ointsub _ _ _ q') ?bigcup_ointsubxx//.

theories/normedtype_theory/urysohn.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval.
 From mathcomp Require Import archimedean.
@@ -85,7 +85,7 @@ Lemma edist_finP (xy : X * X) :
   (edist xy \is a fin_num)%E <-> exists2 r, 0 < r & ball xy.1 r xy.2.
 Proof.
 rewrite ge0_fin_numE ?edist_ge0// ltey.
-rewrite -(rwP (negPP eqP)); apply/iff_not2; rewrite notE.
+rewrite -(rwP (negPP eqP)); apply/iff_not2; rewrite not_notE.
 apply: (iff_trans (edist_pinftyP _)); apply: (iff_trans _ (forall2NP _ _)).
 by under eq_forall => ? do rewrite implyE.
 Qed.

theories/sequences.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp Require Import interval interval_inference archimedean.
@@ -2899,7 +2899,7 @@ have akN1A : a_ k.-1 \in A.
     contra: aiB => ->.
     rewrite /a_ !mul0r addr0; apply/negP => /set_mem/(ABlt _ _ aA).
     by rewrite ltxx.
-  apply/mem_set/boolp.notP => abs.
+  apply/mem_set/not_notP => abs.
   have {}abs : a_ i.-1 \in B.
     by move/seteqP : ABT => [_ /(_ (a_ i.-1) Logic.I)] [//|/mem_set].
   have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW.
@@ -3253,7 +3253,7 @@ have majball g x : F g -> (ball x0 r%:num) x -> `|g (x - x0)| <= n%:R + n%:R.
   move: (linearB (pack_linear Lg)) => /= -> Ballx.
   apply/(le_trans (ler_normB _ _))/lerD; first exact: majballi.
   by apply: majballi => //; exact/ball_center.
-have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y  + x0).
+have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y + x0).
   rewrite -ball_normE /ball_ /= opprD addrC subrK normrN normrZ.
   rewrite 2!normrM 2!normfV normr_id !mulrA divfK ?normr_eq0//.
   by rewrite !gtr0_norm// gtr_pMl// invf_lt1// ltr1n.