addressing comments

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -36,7 +36,7 @@
   + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed)
 
 - in `mathcomp_extra.v`:
-  + lemma `prodr_ile1`
+  + lemmas `prodr_ile1`, `nat_int`
 
 - in `normedtype.v`:
   + lemma `scaler1`
@@ -49,6 +49,11 @@
 - in `lebesgue_integral.v`:
   + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
 
+- new file `pi_irrational.v`:
+  + lemmas `measurable_poly`
+  + module `pi_irrational`
+  + lemma `pi_irrationnal`
+
 ### Changed
 
 - in `lebesgue_integrale.v`

_CoqProject

@@ -89,6 +89,7 @@ theories/probability.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v
+theories/pi_irrational.v
 theories/showcase/summability.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v

classical/mathcomp_extra.v

@@ -501,6 +501,9 @@ End floor_ceil.
 #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")]
 Notation ceil_lt_int := ceil_gt_int (only parsing).
 
+Lemma nat_int {R : archiNumDomainType} n : n%:R \is a @Num.int R.
+Proof. by rewrite Num.Theory.intrEge0. Qed.
+
 Section bijection_forall.
 
 Lemma bij_forall A B (f : A -> B) (P : B -> Prop) :

theories/Make

@@ -57,4 +57,5 @@ convex.v
 charge.v
 kernel.v
 all_analysis.v
+pi_irrational.v
 showcase/summability.v