aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_lemma_N.html
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-22 13:43:08 +0200
committerEnrico Tassi2019-05-22 15:34:14 +0200
commit748d716efb2f2f75946c8386e441ce1789806a39 (patch)
treefe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_lemma_N.html
parent415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_lemma_N.html')
-rw-r--r--docs/htmldoc/index_lemma_N.html160
1 files changed, 100 insertions, 60 deletions
diff --git a/docs/htmldoc/index_lemma_N.html b/docs/htmldoc/index_lemma_N.html
index 7d12494..e6b2218 100644
--- a/docs/htmldoc/index_lemma_N.html
+++ b/docs/htmldoc/index_lemma_N.html
@@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
-<title>mathcomp.ssreflect.tuple</title>
+<title>mathcomp.test_suite.hierarchy_test</title>
</head>
<body>
@@ -47,7 +47,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -79,14 +79,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -111,7 +111,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -143,7 +143,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -175,7 +175,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -207,7 +207,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -239,7 +239,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -271,7 +271,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -303,14 +303,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -335,7 +335,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -367,7 +367,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -399,7 +399,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -431,14 +431,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -463,7 +463,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
<hr/><a name="lemma_N"></a><h2>N (lemma)</h2>
@@ -491,8 +491,9 @@
<a href="mathcomp.ssreflect.ssrnat.html#nat_of_exp_bin">nat_of_exp_bin</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#nat_of_mul_bin">nat_of_mul_bin</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#nat_of_add_bin">nat_of_add_bin</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#nat_of_addn_gt0">nat_of_addn_gt0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#nat_of_succ_gt0">nat_of_succ_gt0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#nat_of_mul_pos">nat_of_mul_pos</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#nat_of_add_pos">nat_of_add_pos</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#nat_of_succ_pos">nat_of_succ_pos</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#nat_of_binK">nat_of_binK</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#nat_AGM2">nat_AGM2</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#nat_Cauchy">nat_Cauchy</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
@@ -554,6 +555,8 @@
<a href="mathcomp.ssreflect.path.html#next_prev">next_prev</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
<a href="mathcomp.ssreflect.path.html#next_cycle">next_cycle</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
<a href="mathcomp.ssreflect.path.html#next_nth">next_nth</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#nhomo_inj_lt_in">nhomo_inj_lt_in</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#nhomo_inj_lt">nhomo_inj_lt</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#nilP">nilP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.solvable.nilpotent.html#nilpotentS">nilpotentS</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
<a href="mathcomp.solvable.maximal.html#nilpotent_Fitting">nilpotent_Fitting</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/>
@@ -704,6 +707,7 @@
<a href="mathcomp.field.falgebra.html#not_asubv0">not_asubv0</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#nseqP">nseqP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.tuple.html#nseq_tupleP">nseq_tupleP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#nthK">nthK</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#nthP">nthP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.path.html#nth_traject">nth_traject</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
<a href="mathcomp.ssreflect.tuple.html#nth_mktuple">nth_mktuple</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
@@ -820,6 +824,8 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.addr_ss_eq0">Num.Theory.addr_ss_eq0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.addr_ge0">Num.Theory.addr_ge0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.archi_boundP">Num.Theory.archi_boundP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_maxrP">Num.Theory.arg_maxrP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_minrP">Num.Theory.arg_minrP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Cauchy_root_bound">Num.Theory.Cauchy_root_bound</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.char_num">Num.Theory.char_num</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.conjCi">Num.Theory.conjCi</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -839,6 +845,12 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Creal_Im">Num.Theory.Creal_Im</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Creal_Re">Num.Theory.Creal_Re</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Crect">Num.Theory.Crect</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decnr_inj_inj_in">Num.Theory.decnr_inj_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decnr_inj_inj">Num.Theory.decnr_inj_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decrn_inj_in">Num.Theory.decrn_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decrn_inj">Num.Theory.decrn_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decr_inj_in">Num.Theory.decr_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decr_inj">Num.Theory.decr_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.distrC">Num.Theory.distrC</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.divr_gt0">Num.Theory.divr_gt0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.divr_ge0">Num.Theory.divr_ge0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -911,12 +923,6 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.gtr0_sg">Num.Theory.gtr0_sg</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.gtr0_real">Num.Theory.gtr0_real</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.gt0_cp">Num.Theory.gt0_cp</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_mono_in">Num.Theory.homo_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_mono">Num.Theory.homo_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_leq_mono">Num.Theory.homo_leq_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_ltn_lt">Num.Theory.homo_inj_ltn_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_in_lt">Num.Theory.homo_inj_in_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_lt">Num.Theory.homo_inj_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ieexprIn">Num.Theory.ieexprIn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ieexprn_weq1">Num.Theory.ieexprn_weq1</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.imaginaryCE">Num.Theory.imaginaryCE</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -927,6 +933,24 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_conj">Num.Theory.Im_conj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_i">Num.Theory.Im_i</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_is_additive">Num.Theory.Im_is_additive</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incnr_inj_in">Num.Theory.incnr_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incnr_inj">Num.Theory.incnr_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incrn_inj_in">Num.Theory.incrn_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incrn_inj">Num.Theory.incrn_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incr_inj_in">Num.Theory.incr_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incr_inj">Num.Theory.incr_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltrn_in">Num.Theory.inj_nhomo_ltrn_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltrn_in">Num.Theory.inj_homo_ltrn_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltrn">Num.Theory.inj_nhomo_ltrn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltrn">Num.Theory.inj_homo_ltrn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltnr_in">Num.Theory.inj_nhomo_ltnr_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltnr_in">Num.Theory.inj_homo_ltnr_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltnr">Num.Theory.inj_nhomo_ltnr</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltnr">Num.Theory.inj_homo_ltnr</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltr_in">Num.Theory.inj_nhomo_ltr_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltr_in">Num.Theory.inj_homo_ltr_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltr">Num.Theory.inj_nhomo_ltr</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltr">Num.Theory.inj_homo_ltr</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.invCi">Num.Theory.invCi</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.invC_rect">Num.Theory.invC_rect</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.invC_norm">Num.Theory.invC_norm</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -945,10 +969,14 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.invr_gt0">Num.Theory.invr_gt0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lef_ninv">Num.Theory.lef_ninv</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lef_pinv">Num.Theory.lef_pinv</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_lerW_nmono">Num.Theory.leq_lerW_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_lerW_mono">Num.Theory.leq_lerW_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_nmono_inj">Num.Theory.leq_nmono_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_mono_inj">Num.Theory.leq_mono_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_nmono_in">Num.Theory.lenrW_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_mono_in">Num.Theory.lenrW_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_nmono">Num.Theory.lenrW_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_mono">Num.Theory.lenrW_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_nmono_in">Num.Theory.lenr_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_mono_in">Num.Theory.lenr_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_nmono">Num.Theory.lenr_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_mono">Num.Theory.lenr_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerifP">Num.Theory.lerifP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_rootC_AGM">Num.Theory.lerif_rootC_AGM</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_Re_Creal">Num.Theory.lerif_Re_Creal</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -973,6 +1001,14 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_trans">Num.Theory.lerif_trans</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_refl">Num.Theory.lerif_refl</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerNgt">Num.Theory.lerNgt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_nmono_in">Num.Theory.lernW_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_mono_in">Num.Theory.lernW_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_nmono">Num.Theory.lernW_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_mono">Num.Theory.lernW_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_nmono_in">Num.Theory.lern_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_mono_in">Num.Theory.lern_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_nmono">Num.Theory.lern_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_mono">Num.Theory.lern_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern0">Num.Theory.lern0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern1">Num.Theory.lern1</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerN10">Num.Theory.lerN10</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -997,6 +1033,10 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_normlP">Num.Theory.ler_normlP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_norml">Num.Theory.ler_norml</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_norm">Num.Theory.ler_norm</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_nmono_in">Num.Theory.ler_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_mono_in">Num.Theory.ler_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_nmono">Num.Theory.ler_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_mono">Num.Theory.ler_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_total">Num.Theory.ler_total</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_ndivr_mull">Num.Theory.ler_ndivr_mull</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_ndivl_mull">Num.Theory.ler_ndivl_mull</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1100,11 +1140,17 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.le0_cp">Num.Theory.le0_cp</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltf_ninv">Num.Theory.ltf_ninv</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltf_pinv">Num.Theory.ltf_pinv</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltn_ltrW_nhomo">Num.Theory.ltn_ltrW_nhomo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltn_ltrW_homo">Num.Theory.ltn_ltrW_homo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_nhomo_in">Num.Theory.ltnrW_nhomo_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_homo_in">Num.Theory.ltnrW_homo_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_nhomo">Num.Theory.ltnrW_nhomo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_homo">Num.Theory.ltnrW_homo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrgtP">Num.Theory.ltrgtP</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrgt0P">Num.Theory.ltrgt0P</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrNge">Num.Theory.ltrNge</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_nhomo_in">Num.Theory.ltrnW_nhomo_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_homo_in">Num.Theory.ltrnW_homo_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_nhomo">Num.Theory.ltrnW_nhomo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_homo">Num.Theory.ltrnW_homo</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrn0">Num.Theory.ltrn0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrn1">Num.Theory.ltrn1</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrN10">Num.Theory.ltrN10</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1188,8 +1234,8 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_le_sub">Num.Theory.ltr_le_sub</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add">Num.Theory.ltr_add</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_le_add">Num.Theory.ltr_le_add</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2l">Num.Theory.ltr_add2l</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2r">Num.Theory.ltr_add2r</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2l">Num.Theory.ltr_add2l</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_oppl">Num.Theory.ltr_oppl</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_oppr">Num.Theory.ltr_oppr</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_opp2">Num.Theory.ltr_opp2</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1254,8 +1300,6 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.monic_Cauchy_bound">Num.Theory.monic_Cauchy_bound</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_lerif">Num.Theory.mono_lerif</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_in_lerif">Num.Theory.mono_in_lerif</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_inj_in">Num.Theory.mono_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_inj">Num.Theory.mono_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulC_rect">Num.Theory.mulC_rect</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulrIn">Num.Theory.mulrIn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulrn_wlt0">Num.Theory.mulrn_wlt0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1294,16 +1338,8 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.neqr0_sign">Num.Theory.neqr0_sign</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.neq0Ci">Num.Theory.neq0Ci</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.neq0_mulr_lt0">Num.Theory.neq0_mulr_lt0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_mono_in">Num.Theory.nhomo_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_mono">Num.Theory.nhomo_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_leq_mono">Num.Theory.nhomo_leq_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_ltn_lt">Num.Theory.nhomo_inj_ltn_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_in_lt">Num.Theory.nhomo_inj_in_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_lt">Num.Theory.nhomo_inj_lt</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_lerif">Num.Theory.nmono_lerif</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_in_lerif">Num.Theory.nmono_in_lerif</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_inj_in">Num.Theory.nmono_inj_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
-<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_inj">Num.Theory.nmono_inj</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rle0">Num.Theory.nmulrn_rle0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rge0">Num.Theory.nmulrn_rge0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rgt0">Num.Theory.nmulrn_rgt0</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1414,6 +1450,10 @@
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realN">Num.Theory.realN</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn">Num.Theory.realn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realNEsign">Num.Theory.realNEsign</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_nmono_in">Num.Theory.realn_nmono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_mono_in">Num.Theory.realn_mono_in</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_nmono">Num.Theory.realn_nmono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
+<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_mono">Num.Theory.realn_mono</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realrM">Num.Theory.realrM</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realrMn">Num.Theory.realrMn</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realV">Num.Theory.realV</a> [in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
@@ -1599,7 +1639,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -1631,14 +1671,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -1663,7 +1703,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -1695,7 +1735,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -1727,7 +1767,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -1759,7 +1799,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -1791,7 +1831,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -1823,7 +1863,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -1855,14 +1895,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -1887,7 +1927,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -1919,7 +1959,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -1951,7 +1991,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -1983,14 +2023,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -2015,7 +2055,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
</div>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-08 09:13:36 +0000