Source / pinned edition
rocq
Source of package rocq.order · 9.2
- work
- urn:arxo:rocq.order#Import_Source_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- number
- 9.2
- kind
- urn:arxo:rocq.order#treatise
Import_Edition_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- edition
- urn:arxo:rocq.order#Import_Edition_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://github.com/rocq-prover/stdlib/blob/V9.2.0/theories/QArith/QArith_base.v | text/plain; charset=utf-8 | sha256:d9108f8e6f33e8854da3525c0a41faaa4915ae4dee80a906891962fb65764aa3 | 2026-09-12T20:15:36Z |
Fragments — 3
Stdlib.QArith.QArith_base.Qlt_trans · lemma · referenced by: 1
en · official · sha256:6f27f9698ef82440cc3e6eb4510f7a29e6ef7bef9bccd364ae97e7a01fea2c0b
Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.Referencing norms: Import_Rule_8872a36d422eacd990d2e74a5dc1e191ea3ec7a256f3b7316d1ac7bf9c7121c7
Stdlib.QArith.QArith_base.Qlt_le_weak · lemma · referenced by: 1
en · official · sha256:1731977af5e2421304d222dfefcc9dbdd6c3bc819e169062ec984222f0b01ea8
Lemma Qlt_le_weak x y : x<y -> x<=y.Referencing norms: Import_Rule_c19ccc16514506ba5e9b2d9ffae5559844a67b72b2027eb3b225008346c18387
Stdlib.QArith.QArith_base.Qle_lt_trans · lemma · referenced by: 1
en · official · sha256:02ce79602f950be5928e29c546301735a6a242fe740669570df42c5b7cc83ca7
Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.Referencing norms: Import_Rule_ffcef37c25169dbe372b14baf1a8bf6f49b69f80e6aa33f3274414942b069a10
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.