--- /srv/rebuilderd/tmp/rebuilderdy9ZXOt/inputs/libcoq-stdlib_8.20.1+dfsg-1+b4_amd64.deb
+++ /srv/rebuilderd/tmp/rebuilderdy9ZXOt/out/libcoq-stdlib_8.20.1+dfsg-1+b4_amd64.deb
├── file list
│ @@ -1,3 +1,3 @@
│ -rw-r--r-- 0 0 0 4 2026-06-19 05:33:29.000000 debian-binary
│ --rw-r--r-- 0 0 0 63084 2026-06-19 05:33:29.000000 control.tar.xz
│ --rw-r--r-- 0 0 0 23462556 2026-06-19 05:33:29.000000 data.tar.xz
│ +-rw-r--r-- 0 0 0 63060 2026-06-19 05:33:29.000000 control.tar.xz
│ +-rw-r--r-- 0 0 0 23462676 2026-06-19 05:33:29.000000 data.tar.xz
├── control.tar.xz
│ ├── control.tar
│ │ ├── ./md5sums
│ │ │ ├── ./md5sums
│ │ │ │┄ Files differ
├── data.tar.xz
│ ├── data.tar
│ │ ├── file list
│ │ │ @@ -2433,91 +2433,91 @@
│ │ │ -rw-r--r-- 0 root (0) root (0) 13021 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.EqNat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 13946 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.Euclid.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 7289 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.Factorial.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 359580 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.PeanoNat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8974 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.Peano_dec.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 79061 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.Wf_nat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 40548 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Array.PArray.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 228745 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Bool.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 228730 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Bool.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 16144 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.BoolEq.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 28690 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.BoolOrder.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 28687 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.BoolOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 34692 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Bvector.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 10524 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.DecBool.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14176 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.IfProp.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 22507 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Sumbool.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9445 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Zerob.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 33297 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CEquivalence.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 153007 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CMorphisms.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 95260 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CRelationClasses.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 14696 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.DecidableClass.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 41301 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.EquivDec.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 33255 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Equivalence.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 6906 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Init.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 161747 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 26018 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Prop.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 15025 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Relations.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 129670 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.RelationClasses.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 61888 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.RelationPairs.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 27487 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidClass.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 32904 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidDec.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 33427 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidTactics.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 33296 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CEquivalence.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 153005 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CMorphisms.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 95257 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CRelationClasses.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 14695 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.DecidableClass.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 41300 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.EquivDec.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 33254 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Equivalence.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 6905 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Init.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 161745 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 26017 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Prop.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 15024 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Relations.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 129667 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.RelationClasses.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 61887 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.RelationPairs.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 27486 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidClass.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 32903 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidDec.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 33426 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.SetoidTactics.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3600 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Compat.AdmitAxiom.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 36191 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Compat.Coq818.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2919 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Compat.Coq819.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2701 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Compat.Coq820.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 638862 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapAVL.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 491502 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapFacts.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 249562 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapFullAVL.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 134223 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapInterface.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 312575 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapList.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 272481 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapPositive.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 273130 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapWeakList.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 638817 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapAVL.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 491484 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapFacts.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 249549 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapFullAVL.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 134217 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapInterface.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 312563 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapList.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 272480 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapPositive.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 273119 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMapWeakList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4419 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FMaps.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 8981 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetAVL.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 241121 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetBridge.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 241710 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetCompat.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 253724 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetDecide.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 244693 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetEqProperties.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 98373 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetFacts.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 229599 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetInterface.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 5846 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetList.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 8980 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetAVL.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 241118 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetBridge.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 241705 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetCompat.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 253708 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetDecide.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 244692 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetEqProperties.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 98369 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetFacts.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 229591 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetInterface.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 5845 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 284090 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetPositive.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 330854 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetProperties.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 30504 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetToFiniteSet.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 6059 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetWeakList.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 330840 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetProperties.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 30502 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetToFiniteSet.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 6058 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSetWeakList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 5771 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.FSets.FSets.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 43973 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.FloatAxioms.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3707 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.FloatClass.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8315 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.FloatLemmas.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 21338 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.FloatOps.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 5273 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.Floats.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 29750 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.PrimFloat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 160762 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Floats.SpecFloat.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 709027 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Byte.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 124437 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Datatypes.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 67743 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Decimal.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 83098 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Hexadecimal.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 532729 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Logic.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 709026 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Byte.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 124431 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Datatypes.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 67742 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Decimal.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 83097 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Hexadecimal.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 532725 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Logic.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2829 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Ltac.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 124867 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Nat.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 124863 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Nat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23171 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Notations.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9933 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Number.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 64638 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Peano.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 12568 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Prelude.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 588062 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Specif.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 69736 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Tactics.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 24852 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Tauto.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 56558 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Init.Wf.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 1005691 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.List.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 1005652 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.List.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23118 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.ListDec.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 113626 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.ListSet.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 15205 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.ListTactics.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 236380 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.SetoidList.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 236379 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.SetoidList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 44917 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.SetoidPermutation.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 37550 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.StreamMemo.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 37549 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.StreamMemo.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 57012 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Lists.Streams.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 54223 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.Adjointification.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 28317 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.Berardi.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 238047 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.ChoiceFacts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3121 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.Classical.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 13475 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.ClassicalChoice.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23909 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.ClassicalDescription.html
│ │ │ @@ -2550,145 +2550,145 @@
│ │ │ -rw-r--r-- 0 root (0) root (0) 7646 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.RelationalChoice.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3397 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.SetIsType.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 17187 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.SetoidChoice.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9458 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.StrictProp.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 57550 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.WKL.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23285 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Logic.WeakFan.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 198582 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetAVL.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 253506 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetDecide.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 253490 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetDecide.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 245421 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetEqProperties.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 147620 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetFacts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 239860 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetGenTree.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 345771 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetInterface.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 345764 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetInterface.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 203409 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 233427 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetPositive.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 332281 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetProperties.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 463865 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetRBT.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 463850 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetRBT.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 30363 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetToFiniteSet.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 127905 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSetWeakList.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 5306 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.MSets.MSets.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 281095 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.BinNat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 99064 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.BinNatDef.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 7411 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.NArith.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 88281 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.Ndec.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8571 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.Ndiv_def.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 6254 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.Ngcd_def.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 69143 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.Nnat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3820 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.NArith.Nsqrt_def.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 11733 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.AltBinNotations.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 15561 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.BinNums.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 11734 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.AltBinNotations.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 15562 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.BinNums.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4226 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.CarryType.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 210248 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.CyclicAxioms.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 210249 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.CyclicAxioms.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14968 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.DoubleType.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 54727 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.NZCyclic.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 77296 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Cyclic63.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 54728 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Abstract.NZCyclic.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 77297 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Cyclic63.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 18492 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.PrimInt63.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 19222 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Ring63.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 19223 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Ring63.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 103930 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Sint63.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 476321 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Cyclic.Int63.Uint63.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 151918 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalFacts.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 20858 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalN.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 60110 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalNat.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 78256 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalPos.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 52837 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalQ.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 16563 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalR.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 56969 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalString.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 17290 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalZ.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 164470 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalFacts.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 21324 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalN.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 72169 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalNat.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 94746 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalPos.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 54915 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalQ.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 17388 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalR.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 69145 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalString.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 22472 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalZ.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 151919 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalFacts.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 20859 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalN.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 60111 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalNat.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 78257 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalPos.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 52838 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalQ.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 16564 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalR.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 56970 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalString.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 17291 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.DecimalZ.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 164471 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalFacts.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 21325 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalN.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 72170 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalNat.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 94747 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalPos.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 54916 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalQ.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 17389 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalR.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 69146 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalString.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 22473 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.HexadecimalZ.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 81809 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZAdd.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 89793 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZAddOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 52844 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZAxioms.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 7577 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZBase.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 411948 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZBits.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 169042 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivEucl.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 198034 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivFloor.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 187482 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivTrunc.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 411949 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZBits.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 169046 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivEucl.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 198038 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivFloor.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 187486 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZDivTrunc.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 63229 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZGcd.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 120718 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZLcm.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 120719 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZLcm.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 30570 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZLt.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 50927 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZMaxMin.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 50928 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZMaxMin.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 21231 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZMul.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 57329 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZMulOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 12252 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZParity.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 24386 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZPow.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 11521 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZProperties.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 71260 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Abstract.ZSgnAbs.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 7497 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Binary.ZBinary.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 7498 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.Binary.ZBinary.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 94861 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Integer.NatPairs.ZNatPairs.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 68956 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NaryFunctions.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 33399 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAdd.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 52990 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAddOrder.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 79891 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAxioms.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 21084 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZBase.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 68957 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NaryFunctions.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 33400 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAdd.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 52991 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAddOrder.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 79896 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZAxioms.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 21085 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZBase.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 43896 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZBits.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 158101 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZDiv.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 79372 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZDomain.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 158104 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZDiv.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 79375 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZDomain.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 87001 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZGcd.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 136194 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZLog.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 30861 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZMul.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 108117 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZMulOrder.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 159233 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZOrder.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 136195 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZLog.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 30862 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZMul.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 108118 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZMulOrder.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 159243 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 54302 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZParity.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 81095 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZPow.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3531 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZProperties.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 118563 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZSqrt.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 118564 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NatInt.NZSqrt.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 17347 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NAdd.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 11677 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NAddOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 25697 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NAxioms.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 41537 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NBase.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 391421 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NBits.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 82587 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NDefOps.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 128778 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NDiv.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 128781 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NDiv.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 99595 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NDiv0.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 63918 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NGcd.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23500 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NIso.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 72769 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NLcm.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 72770 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NLcm.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 82375 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NLcm0.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 6761 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NLog.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 35614 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NMaxMin.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 35615 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NMaxMin.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23197 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NMulOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 53042 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NOrder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 11515 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NParity.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 66542 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NPow.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 16155 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NProperties.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 34603 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NSqrt.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 47349 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NStrongRec.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 80895 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Abstract.NSub.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 4172 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Binary.NBinary.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 4173 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.Natural.Binary.NBinary.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3751 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Numbers.NumPrelude.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 519325 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.BinPos.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 239659 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.BinPosDef.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 519380 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.BinPos.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 239686 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.BinPosDef.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3194 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.PArith.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 6865 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.POrderedType.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 6868 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.POrderedType.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 108056 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.PArith.Pnat.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 12884 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Basics.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 14855 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Combinators.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 14853 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Combinators.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 104803 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Equality.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4079 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Program.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 22433 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Subset.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 5530 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Syntax.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 54100 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Tactics.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8061 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Utils.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 72801 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Program.Wf.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3205 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.QArith.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 361720 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.QArith_base.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 11508 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.QOrderedType.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 361725 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.QArith_base.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 11511 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.QOrderedType.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 32262 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qabs.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 28740 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qcabs.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 28741 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qcabs.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 123499 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qcanon.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 30429 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qfield.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 16087 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qminmax.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 91983 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qpower.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 30430 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qfield.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 16089 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qminmax.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 92002 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qpower.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 24025 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qreals.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 26743 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qreduction.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2788 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qring.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 18612 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.QArith.Qround.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 42495 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Reals.Abstract.ConstructiveAbs.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 87024 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Reals.Abstract.ConstructiveLUB.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 100172 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Reals.Abstract.ConstructiveLimits.html
│ │ │ @@ -2794,20 +2794,20 @@
│ │ │ -rw-r--r-- 0 root (0) root (0) 19555 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_1.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 23129 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_1_facts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 17551 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_2.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 29642 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_2_facts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 16870 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_3.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14440 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Relations_3_facts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 50873 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sets.Uniset.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 72712 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.CPermutation.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 75081 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Heap.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 72713 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.CPermutation.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 75091 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Heap.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 46174 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Mergesort.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 34335 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.PermutEq.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 111109 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.PermutSetoid.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 213702 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Permutation.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 111112 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.PermutSetoid.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 213703 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Permutation.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 40699 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Sorted.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2999 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Sorting.Sorting.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 72920 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Strings.Ascii.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 40714 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Strings.BinaryString.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 258395 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Strings.Byte.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 95295 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Strings.HexString.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 60524 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Strings.OctalString.html
│ │ │ @@ -2829,69 +2829,69 @@
│ │ │ -rw-r--r-- 0 root (0) root (0) 152994 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Structures.OrdersFacts.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 53020 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Structures.OrdersLists.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 90857 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Structures.OrdersTac.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3975 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Unicode.Utf8.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 10206 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Unicode.Utf8_core.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 105581 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.Fin.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 13340 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.Vector.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 159229 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.VectorDef.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 159231 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.VectorDef.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 18952 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.VectorEq.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 228255 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.VectorSpec.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 228267 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Vectors.VectorSpec.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 10522 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Disjoint_Union.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 7688 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Inclusion.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 16357 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Inverse_Image.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 36848 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Lexicographic_Exponentiation.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 33731 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Lexicographic_Product.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9750 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Transitive_Closure.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14007 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Union.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 16919 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Well_Ordering.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4392 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.Wellfounded.Wellfounded.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 457859 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.BinInt.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 189038 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.BinIntDef.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 176738 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Int.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 189041 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.BinIntDef.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 176742 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Int.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 52637 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Wf_Z.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4978 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.ZArith.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 7451 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.ZArith_base.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 44088 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.ZArith_dec.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 26763 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zabs.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 77261 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zbitwise.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 56078 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zbool.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 58960 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zcompare.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 44090 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.ZArith_dec.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 26766 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zabs.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 77265 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zbitwise.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 56080 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zbool.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 58968 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zcompare.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 28671 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zcomplements.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 225885 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zdiv.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 14889 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zeuclid.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 60510 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zeven.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 38842 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zgcd_alt.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 9585 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zhints.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 225894 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zdiv.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 14890 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zeuclid.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 60511 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zeven.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 38843 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zgcd_alt.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 9588 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zhints.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14641 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zmax.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 14380 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zmin.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 3187 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zminmax.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 6421 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zmisc.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 270640 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Znat.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 194863 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Znumtheory.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 163636 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zorder.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 270643 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Znat.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 194868 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Znumtheory.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 163646 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zorder.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 18204 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpow_alt.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 6595 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpow_def.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 56492 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpow_facts.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 84256 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpower.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 129130 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zquot.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 6596 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpow_def.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 56494 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpow_facts.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 84259 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zpower.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 129135 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zquot.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 12888 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.Zwf.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 23777 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.auxiliary.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 132777 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.btauto.Algebra.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 23778 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.ZArith.auxiliary.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 132779 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.btauto.Algebra.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2892 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.btauto.Btauto.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 61132 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.btauto.Reflect.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 2582 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.derive.Derive.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 5557 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellBasic.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4337 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellNatInt.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4348 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellNatInteger.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8859 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellNatNum.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 10079 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellString.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 4992 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellZInt.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 4995 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellZInt.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4886 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellZInteger.html
│ │ │ --rw-r--r-- 0 root (0) root (0) 6083 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellZNum.html
│ │ │ +-rw-r--r-- 0 root (0) root (0) 6088 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrHaskellZNum.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9860 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOCamlFloats.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 9832 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOCamlInt63.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 4484 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOCamlPArray.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 6560 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOCamlPString.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 6092 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOcamlBasic.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 8544 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOcamlChar.html
│ │ │ -rw-r--r-- 0 root (0) root (0) 26596 2026-06-19 05:33:29.000000 ./usr/share/doc/libcoq-stdlib/html/Coq.extraction.ExtrOcamlIntConv.html
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.Arith_base.html
│ │ │ @@ -54,15 +54,15 @@
│ │ │ Require Export EqNat.
│ │ │ Require Export Wf_nat.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
arith hint database
│ │ │ +
arith hint database
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ #[global]
│ │ │ Hint Resolve eq_nat_refl: arith.
│ │ │ @@ -76,15 +76,15 @@
│ │ │ #[global]
│ │ │ Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
lt and le
│ │ │ +
lt and le
│ │ │
│ │ │
│ │ │ #[global]
│ │ │ Hint Resolve Nat.le_trans: arith. #[global]
│ │ │ Hint Immediate Nat.le_antisymm: arith. #[global]
│ │ │ Hint Resolve Nat.le_0_l Nat.nle_succ_0: arith. #[global]
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Arith.EqNat.html
│ │ │ @@ -52,15 +52,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Equality on natural numbers
│ │ │
│ │ │
│ │ │ -
Propositional equality
│ │ │ +
Propositional equality
│ │ │
│ │ │
│ │ │ -
Remaining constants not defined in Coq.Init.Nat
│ │ │ +
Remaining constants not defined in Coq.Init.Nat
│ │ │
│ │ │
│ │ │
│ │ │ NB: Aliasing
le is mandatory, since only a Definition can implement
│ │ │ an interface Parameter...
│ │ │
│ │ │ @@ -163,15 +163,15 @@
│ │ │
Definition le :=
Peano.le.
│ │ │
Definition lt :=
Peano.lt.
│ │ │
│ │ │
│ │ │
│ │ │ -
Basic specifications : pred add sub mul
│ │ │ +
Basic specifications : pred add sub mul
│ │ │
│ │ │
│ │ │ -
Boolean comparisons
│ │ │ +
Boolean comparisons
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
Lemma eqb_eq n m :
eqb n m = true <-> n = m.
│ │ │
│ │ │ @@ -237,27 +237,27 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Decidability of equality over nat.
│ │ │ +
Decidability of equality over nat.
│ │ │
│ │ │
│ │ │ -
Ternary comparison
│ │ │ +
Ternary comparison
│ │ │
│ │ │
│ │ │
│ │ │ With
nat, it would be easier to prove first
compare_spec,
│ │ │ then the properties below. But then we wouldn't be able to
│ │ │ benefit from functor
BoolOrderFacts
│ │ │
│ │ │ Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Minimum, maximum
│ │ │ +
Minimum, maximum
│ │ │
│ │ │
│ │ │ -
Power
│ │ │ +
Power
│ │ │
│ │ │
│ │ │ -
Square
│ │ │ +
Square
│ │ │
│ │ │
│ │ │ -
Parity
│ │ │ +
Parity
│ │ │
│ │ │
│ │ │ -
Division
│ │ │ +
Division
│ │ │
│ │ │
│ │ │ -
Square root
│ │ │ +
Square root
│ │ │
│ │ │
│ │ │ -
Logarithm
│ │ │ +
Logarithm
│ │ │
│ │ │
│ │ │ -
Properties of iter
│ │ │ +
Properties of iter
│ │ │
│ │ │
│ │ │ -
Gcd
│ │ │ +
Gcd
│ │ │
│ │ │
│ │ │ -
Bitwise operations
│ │ │ +
Bitwise operations
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
Definition double_S :
forall n,
double (
S n)
= S (
S (
double n))
│ │ │ :=
fun n =>
add_succ_r (
S n)
n.
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.Bool.html
│ │ │ @@ -86,27 +86,27 @@
│ │ │ |
false =>
False
│ │ │
end.
│ │ │
│ │ │
│ │ │
│ │ │ -
Decidability
│ │ │ +
Decidability
│ │ │
│ │ │
│ │ │ -
Discrimination
│ │ │ +
Discrimination
│ │ │
│ │ │
│ │ │ -
Order on booleans
│ │ │ +
Order on booleans
│ │ │
│ │ │
│ │ │ -
Equality
│ │ │ +
Equality
│ │ │
│ │ │
│ │ │ -
A synonym of if on bool
│ │ │ +
A synonym of if on bool
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
Definition ifb (
b1 b2 b3:
bool) :
bool :=
│ │ │
match b1 with
│ │ │ @@ -238,30 +238,30 @@
│ │ │
│ │ │
Open Scope bool_scope.
│ │ │
│ │ │
│ │ │
│ │ │ -
De Morgan laws
│ │ │ +
De Morgan laws
│ │ │
│ │ │
│ │ │ -
Properties of negb
│ │ │ +
Properties of negb
│ │ │
│ │ │
│ │ │ -
Properties of orb
│ │ │ +
Properties of orb
│ │ │
│ │ │
│ │ │ -
Properties of andb
│ │ │ +
Properties of andb
│ │ │
│ │ │
│ │ │ -
Properties mixing andb and orb
│ │ │ +
Properties mixing andb and orb
│ │ │
│ │ │
│ │ │
│ │ │ Distributivity
│ │ │
│ │ │
│ │ │ @@ -590,15 +590,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Properties of implb
│ │ │ +
Properties of implb
│ │ │
│ │ │
│ │ │ -
Properties of xorb
│ │ │ +
Properties of xorb
│ │ │
│ │ │
│ │ │
│ │ │
false is neutral for
xorb
│ │ │
│ │ │
│ │ │ @@ -806,15 +806,15 @@
│ │ │ #[global]
│ │ │ Hint Resolve trans_eq_bool : core.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Reflection of bool into Prop
│ │ │ +
Reflection of bool into Prop
│ │ │
│ │ │
│ │ │
│ │ │
Is_true and equality
│ │ │
│ │ │
│ │ │ @@ -920,15 +920,15 @@
│ │ │
(if negb b then a else a') =
│ │ │
(if b then a' else a).
│ │ │
│ │ │
│ │ │
│ │ │ -
Alternative versions of andb and orb
│ │ │ +
Alternative versions of andb and orb
│ │ │
│ │ │ with lazy behavior (for vm_compute)
│ │ │
│ │ │
│ │ │
│ │ │
Declare Scope lazy_bool_scope.
│ │ │ @@ -948,15 +948,15 @@
│ │ │
│ │ │
Lemma orb_lazy_alt :
forall a b :
bool,
a || b = a ||| b.
│ │ │
│ │ │
│ │ │
│ │ │ -
Reflect: a specialized inductive type for
│ │ │ +
Reflect: a specialized inductive type for
│ │ │
│ │ │ relating propositions and booleans,
│ │ │ as popularized by the Ssreflect library.
│ │ │
│ │ │
│ │ │
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Bool.BoolOrder.html
│ │ │ @@ -62,15 +62,15 @@
│ │ │
Import BoolNotations.
│ │ │
Local Ltac Tauto.intuition_solver ::=
auto with typeclass_instances relations.
│ │ │
│ │ │
│ │ │
│ │ │ -
Order le
│ │ │ +
Order le
│ │ │
│ │ │
│ │ │ -
Strict order lt
│ │ │ +
Strict order lt
│ │ │
│ │ │
│ │ │ -
Order structures
│ │ │ +
Order structures
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ #[
global]
│ │ │
Instance le_preorder :
PreOrder Bool.le.
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CEquivalence.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Typeclass-based setoids. Definitions on Equivalence.
│ │ │ +
Typeclass-based setoids. Definitions on Equivalence.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CMorphisms.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Typeclass-based morphism definition and standard, minimal instances
│ │ │ +
Typeclass-based morphism definition and standard, minimal instances
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ │
│ │ │ @@ -74,15 +74,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Morphisms.
│ │ │ +
Morphisms.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ We now turn to the definition of
Proper and declare standard instances.
│ │ │ These will be used by the
setoid_rewrite tactic later.
│ │ │
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.CRelationClasses.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Typeclass-based relations, tactics and standard instances
│ │ │ +
Typeclass-based relations, tactics and standard instances
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ This is the basic theory needed to formalize morphisms and setoids.
│ │ │
│ │ │
│ │ │ @@ -450,15 +450,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ We can already dualize all these properties.
│ │ │
│ │ │
│ │ │ -
Standard instances.
│ │ │ +
Standard instances.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Partial Order.
│ │ │ +
Partial Order.
│ │ │
│ │ │ A partial order is a preorder which is additionally antisymmetric.
│ │ │ We give an equivalent definition, up-to an equivalence crelation
│ │ │ on the carrier.
│ │ │
│ │ │
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.DecidableClass.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
A typeclass to ease the handling of decidable properties.
│ │ │ +
A typeclass to ease the handling of decidable properties.
│ │ │
│ │ │
│ │ │
│ │ │ A proposition is decidable whenever it is reflected by a boolean.
│ │ │
│ │ │
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.EquivDec.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Decidable equivalences.
│ │ │ +
Decidable equivalences.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Equivalence.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Typeclass-based setoids. Definitions on Equivalence.
│ │ │ +
Typeclass-based setoids. Definitions on Equivalence.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Init.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Initialization code for typeclasses, setting up the default tactic
│ │ │ +
Initialization code for typeclasses, setting up the default tactic
│ │ │
│ │ │ for instance search.
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Typeclass-based morphism definition and standard, minimal instances
│ │ │ +
Typeclass-based morphism definition and standard, minimal instances
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ │
│ │ │ @@ -70,15 +70,15 @@
│ │ │
Generalizable Variables A eqA B C D R RA RB RC m f x y.
│ │ │
Local Obligation Tactic :=
try solve [
simpl_relation ].
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Morphisms.
│ │ │ +
Morphisms.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ We now turn to the definition of
Proper and declare standard instances.
│ │ │ These will be used by the
setoid_rewrite tactic later.
│ │ │
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Prop.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ -
Proper instances for propositional connectives.
│ │ │ +
Proper instances for propositional connectives.
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │ Author: Matthieu Sozeau
│ │ │ Institution: LRI, CNRS UMR 8623 - University Paris Sud
│ │ ├── ./usr/share/doc/libcoq-stdlib/html/Coq.Classes.Morphisms_Relations.html
│ │ │ @@ -45,15 +45,15 @@
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
│ │ │
..
.Vario
│ │ │ -00003d10: 7573 2063 6f6d 6269 6e61 7469 6f6e 7320 us combinations
│ │ │ -00003d20: 6f66 2072 6566 6c65 7869 7669 7479 2c20 of reflexivity,
│ │ │ -00003d30: 7379 6d6d 6574 7279 2061 6e64 2074 7261 symmetry and tra
│ │ │ -00003d40: 6e73 6974 6976 6974 792e 200a 3c64 6976 nsitivity. .
.. A <
│ │ │ -00003d70: 7370 616e 2063 6c61 7373 3d22 696e 6c69 span class="inli
│ │ │ -00003d80: 6e65 636f 6465 223e 3c73 7061 6e20 636c necode">
PreOrder is b
│ │ │ -00003dc0: 6f74 6820 5265 666c 6578 6976 6520 616e oth Reflexive an
│ │ │ -00003dd0: 6420 5472 616e 7369 7469 7665 2e20 0a3c d Transitive. .<
│ │ │ -00003de0: 2f64 6976 3e0a 3c64 6976 2063 6c61 7373 /div>.
.
│ │ │ -000043b0: 0a3c 6469 7620 636c 6173 733d 2264 6f63 .
.A Stric
│ │ │ -00004400: 744f 7264 6572 3c2f 7370 616e 3e3c 2f73 tOrder is both Irr
│ │ │ -00004420: 6566 6c65 7869 7665 2061 6e64 2054 7261 eflexive and Tra
│ │ │ -00004430: 6e73 6974 6976 652e 200a 3c2f 6469 763e nsitive. .
│ │ │ -00004440: 0a3c 6469 7620 636c 6173 733d 2263 6f64 .
..
.By de
│ │ │ -00004a40: 6669 6e69 7469 6f6e 2c20 6120 7374 7269 finition, a stri
│ │ │ -00004a50: 6374 206f 7264 6572 2069 7320 616c 736f ct order is also
│ │ │ -00004a60: 2061 7379 6d6d 6574 7269 6320 0a3c 2f64 asymmetric ..
│ │ │ -00004d30: 0a0a 3c64 6976 2063 6c61 7373 3d22 646f ..
.A partial eq
│ │ │ -00004d50: 7569 7661 6c65 6e63 6520 7265 6c61 7469 uivalence relati
│ │ │ -00004d60: 6f6e 2069 7320 5379 6d6d 6574 7269 6320 on is Symmetric
│ │ │ -00004d70: 616e 6420 5472 616e 7369 7469 7665 2e20 and Transitive.
│ │ │ -00004d80: 0a3c 2f64 6976 3e0a 3c64 6976 2063 6c61 .
.
..
.
C
│ │ │ -00004dd0: 6c61 7373 3c2f 7370 616e 3e20 3c61 2069 lass PER
│ │ │ -00004e30: 2028 3c61 2069 643d 2252 3a33 3922 2063 (R : relation A) :
Pro
│ │ │ -00004fa0: 703c 2f73 7061 6e3e 203a 3d20 7b3c 6272 p := {
. &
│ │ │ -00004fc0: 6e62 7370 3b26 6e62 7370 3b23 5b3c 7370 nbsp; #[global
│ │ │ -00004ff0: 3c2f 7370 616e 3e5d 203c 6120 6964 3d22 ] PER_Symme
│ │ │ -00005060: 7472 6963 3c2f 7370 616e 3e3c 2f61 3e20 tric
│ │ │ -00005070: 3a3a 203c 6120 636c 6173 733d 2269 6472 :: Symmetric R | 3 ;
. &n
│ │ │ -00005170: 6273 703b 266e 6273 703b 235b 3c73 7061 bsp; #[
global<
│ │ │ -000051a0: 2f73 7061 6e3e 5d20 3c61 2069 643d 2250 /span>] PER_Tran
│ │ │ -00005210: 7369 7469 7665 3c2f 7370 616e 3e3c 2f61 sitive :: Transiti
│ │ │ -00005290: 7665 3c2f 7370 616e 3e3c 2f61 3e20 3c61 ve R<
│ │ │ -00005300: 2f73 7061 6e3e 3c2f 613e 207c 2033 207d /span> | 3 }
│ │ │ -00005310: 2e3c 6272 2f3e 0a0a 3c62 722f 3e0a 3c2f .
..
....Equivale
│ │ │ -00005340: 6e63 6520 7265 6c61 7469 6f6e 732e 200a nce relations. .
│ │ │ -00005350: 3c2f 6469 763e 0a3c 6469 7620 636c 6173
....An Equ
│ │ │ -00005b10: 6976 616c 656e 6365 2069 7320 6120 5045 ivalence is a PE
│ │ │ -00005b20: 5220 706c 7573 2072 6566 6c65 7869 7669 R plus reflexivi
│ │ │ -00005b30: 7479 2e20 0a3c 2f64 6976 3e0a 3c64 6976 ty. .
...
│ │ │ -00005b50: 3c62 722f 3e0a 266e 6273 703b 266e 6273
. &nbs
│ │ │ -00005b60: 703b 3c73 7061 6e20 636c 6173 733d 2269 p;
Global Instan
│ │ │ -00005b90: 6365 3c2f 7370 616e 3e20 3c61 2069 643d ce Equiva
│ │ │ -00005c00: 6c65 6e63 655f 5045 523c 2f73 7061 6e3e lence_PER
│ │ │ -00005c10: 3c2f 613e 207b 3c61 2069 643d 2252 3a34 {
R<
│ │ │ -00005c60: 2f73 7061 6e3e 3c2f 613e 7d20 6028 3c61 /span>} `(
E:Equivalen
│ │ │ -00005d30: 6365 3c2f 7370 616e 3e3c 2f61 3e20 3c61 ce R<
│ │ │ -00005da0: 2f73 7061 6e3e 3c2f 613e 2920 3a20 3c61 /span>) :
PER R | 10 :=
. &
│ │ │ -00005ea0: 6e62 7370 3b26 6e62 7370 3b7b 207d 2e3c nbsp; { }.<
│ │ │ -00005eb0: 6272 2f3e 0a0a 3c62 722f 3e0a 3c2f 6469 br/>..
...
.An Equival
│ │ │ -00005ee0: 656e 6365 2069 7320 6120 5072 654f 7264 ence is a PreOrd
│ │ │ -00005ef0: 6572 2070 6c75 7320 7379 6d6d 6574 7279 er plus symmetry
│ │ │ -00005f00: 2e20 0a3c 2f64 6976 3e0a 3c64 6976 2063 . .
.
..
.We
│ │ │ -000062c0: 6361 6e20 6e6f 7720 6465 6669 6e65 2061 can now define a
│ │ │ -000062d0: 6e74 6973 796d 6d65 7472 7920 772e 722e ntisymmetry w.r.
│ │ │ -000062e0: 742e 2061 6e20 6571 7569 7661 6c65 6e63 t. an equivalenc
│ │ │ -000062f0: 6520 7265 6c61 7469 6f6e 206f 6e20 7468 e relation on th
│ │ │ -00006300: 6520 6361 7272 6965 722e 200a 3c2f 6469 e carrier. ..
..
.Any sy
│ │ │ -00007510: 6d6d 6574 7269 6320 7265 6c61 7469 6f6e mmetric relation
│ │ │ -00007520: 2069 7320 6571 7561 6c20 746f 2069 7473 is equal to its
│ │ │ -00007530: 2069 6e76 6572 7365 2e20 0a3c 2f64 6976 inverse. .
.
│ │ │ -000098b0: 0a0a 3c64 6976 2063 6c61 7373 3d22 646f ..
.Inversing th
│ │ │ -000098d0: 6520 6c61 7267 6572 2073 7472 7563 7475 e larger structu
│ │ │ -000098e0: 7265 7320 0a3c 2f64 6976 3e0a 3c64 6976 res .
.
..
.Rew
│ │ │ -0000ad90: 7269 7465 2072 656c 6174 696f 6e20 6f6e rite relation on
│ │ │ -0000ada0: 2061 2067 6976 656e 2073 7570 706f 7274 a given support
│ │ │ -0000adb0: 3a20 6465 636c 6172 6573 2061 2072 656c : declares a rel
│ │ │ -0000adc0: 6174 696f 6e20 6173 2061 2072 6577 7269 ation as a rewri
│ │ │ -0000add0: 7465 0a20 2020 7265 6c61 7469 6f6e 2066 te. relation f
│ │ │ -0000ade0: 6f72 2075 7365 2062 7920 7468 6520 6765 or use by the ge
│ │ │ -0000adf0: 6e65 7261 6c69 7a65 6420 7265 7772 6974 neralized rewrit
│ │ │ -0000ae00: 696e 6720 7461 6374 6963 2e0a 2020 2049 ing tactic.. I
│ │ │ -0000ae10: 7420 6865 6c70 7320 6368 6f6f 7369 6e67 t helps choosing
│ │ │ -0000ae20: 2069 6620 6120 7265 7772 6974 6520 7368 if a rewrite sh
│ │ │ -0000ae30: 6f75 6c64 2062 6520 6861 6e64 6c65 640a ould be handled.
│ │ │ -0000ae40: 2020 2062 7920 7468 6520 6765 6e65 7261 by the genera
│ │ │ -0000ae50: 6c69 7a65 6420 6f72 2074 6865 2072 6567 lized or the reg
│ │ │ -0000ae60: 756c 6172 2072 6577 7269 7469 6e67 2074 ular rewriting t
│ │ │ -0000ae70: 6163 7469 6320 7573 696e 6720 6c65 6962 actic using leib
│ │ │ -0000ae80: 6e69 7a20 6571 7561 6c69 7479 2e0a 2020 niz equality..
│ │ │ -0000ae90: 2055 7365 7273 2063 616e 2064 6563 6c61 Users can decla
│ │ │ -0000aea0: 7265 2061 6e20 3c73 7061 6e20 636c 6173 re an <
│ │ │ -0000aec0: 7370 616e 2063 6c61 7373 3d22 6964 2220 span class="id"
│ │ │ -0000aed0: 7469 746c 653d 2276 6172 223e 5265 7772 title="var">Rewr
│ │ │ -0000aee0: 6974 6552 656c 6174 696f 6e3c 2f73 7061 iteRelation
│ │ │ -0000af30: 413c 2f73 7061 6e3e 3c2f 7370 616e 3e20 A
│ │ │ -0000af40: 3c73 7061 6e20 636c 6173 733d 2269 6e6c RA<
│ │ │ -0000af80: 2f73 7061 6e3e 2061 6e79 7768 6572 6520 /span> anywhere
│ │ │ -0000af90: 746f 2064 6563 6c61 7265 2064 6566 6175 to declare defau
│ │ │ -0000afa0: 6c74 0a20 2020 7265 6c61 7469 6f6e 7320 lt. relations
│ │ │ -0000afb0: 6f6e 2061 2067 6976 656e 2074 7970 6520 on a given type
│ │ │ -0000afc0: 6041 602e 2054 6869 7320 6973 2061 6c73 `A`. This is als
│ │ │ -0000afd0: 6f20 646f 6e65 2061 7574 6f6d 6174 6963 o done automatic
│ │ │ -0000afe0: 616c 6c79 2062 790a 2020 2074 6865 203c ally by. the <
│ │ │ -0000aff0: 7370 616e 2063 6c61 7373 3d22 696e 6c69 span class="inli
│ │ │ -0000b000: 6e65 636f 6465 223e 3c73 7061 6e20 636c necode">Declare Relation
│ │ │ -0000b080: 3c2f 7370 616e 3e20 3c73 7061 6e20 636c A<
│ │ │ -0000b0c0: 2f73 7061 6e3e 3c2f 7370 616e 3e20 3c73 /span> RA commands. I
│ │ │ -0000b120: 7420 6861 7320 6e6f 206d 6f64 6520 6465 t has no mode de
│ │ │ -0000b130: 636c 6172 6174 696f 6e3a 0a20 2020 6974 claration:. it
│ │ │ -0000b140: 2077 696c 6c20 6173 7369 676e 2060 3f41 will assign `?A
│ │ │ -0000b150: 203a 3d20 5072 6f70 2c20 3f52 203a 3d20 := Prop, ?R :=
│ │ │ -0000b160: 6966 6660 206f 6e20 616e 2065 6e74 6972 iff` on an entir
│ │ │ -0000b170: 656c 7920 756e 7370 6563 6966 6965 6420 ely unspecified
│ │ │ -0000b180: 7175 6572 790a 2020 2060 5265 7772 6974 query. `Rewrit
│ │ │ -0000b190: 6552 656c 6174 696f 6e20 3f41 203f 5260 eRelation ?A ?R`
│ │ │ -0000b1a0: 2c20 6f72 2061 6e79 2070 7265 6665 7265 , or any prefere
│ │ │ -0000b1b0: 6420 7265 7772 6974 6520 7265 6c61 7469 d rewrite relati
│ │ │ -0000b1c0: 6f6e 206f 6620 7072 696f 7269 7479 2026 on of priority &
│ │ │ -0000b1d0: 6c74 3b20 322e 200a 3c2f 6469 763e 0a3c lt; 2. .
.<
│ │ │ -0000b1e0: 6469 7620 636c 6173 733d 2263 6f64 6522 div class="code"
│ │ │ -0000b1f0: 3e0a 0a3c 6272 2f3e 0a26 6e62 7370 3b26 >..
. &
│ │ │ -0000b200: 6e62 7370 3b3c 7370 616e 2063 6c61 7373 nbsp;
Class RewriteRelation
│ │ │ -0000b2a0: 3c2f 7370 616e 3e3c 2f61 3e20 283c 6120 (RA : relation A).
.
│ │ │ -0000b400: 0a3c 6272 2f3e 0a3c 2f64 6976 3e0a 0a3c .
...<
│ │ │ -0000b410: 6469 7620 636c 6173 733d 2264 6f63 223e div class="doc">
│ │ │ -0000b420: 0a4c 6569 626e 697a 2065 7175 616c 6974 .Leibniz equalit
│ │ │ -0000b430: 792e 200a 3c2f 6469 763e 0a3c 6469 7620 y. .
.&n
│ │ │ -0000b450: 6273 703b 266e 6273 703b 3c73 7061 6e20 bsp;
Secti
│ │ │ -0000b480: 6f6e 3c2f 7370 616e 3e20 3c61 2069 643d on Leibniz.
.&nbs
│ │ │ -0000b500: 703b 266e 6273 703b 266e 6273 703b 266e p; &n
│ │ │ -0000b510: 6273 703b 3c73 7061 6e20 636c 6173 733d bsp;
Global Inst
│ │ │ -0000b540: 616e 6365 3c2f 7370 616e 3e20 3c61 2069 ance eq_Reflexi
│ │ │ -0000b5b0: 7665 3c2f 7370 616e 3e3c 2f61 3e20 3a20 ve :
│ │ │ -0000b5c0: 3c61 2063 6c61 7373 3d22 6964 7265 6622
Reflexive (@
eq A) := @
eq_refl A.
.&n
│ │ │ -0000b7f0: 6273 703b 266e 6273 703b 266e 6273 703b bsp;
│ │ │ -0000b800: 266e 6273 703b 3c73 7061 6e20 636c 6173
Global In
│ │ │ -0000b830: 7374 616e 6365 3c2f 7370 616e 3e20 3c61 stance eq_Symme
│ │ │ -0000b8a0: 7472 6963 3c2f 7370 616e 3e3c 2f61 3e20 tric
│ │ │ -0000b8b0: 3a20 3c61 2063 6c61 7373 3d22 6964 7265 :
Symmetric (@
eq<
│ │ │ -0000b980: 2f73 7061 6e3e 3c2f 613e 203c 6120 636c /span> A) := @<
│ │ │ -0000ba00: 6120 636c 6173 733d 2269 6472 6566 2220 a class="idref"
│ │ │ -0000ba10: 6872 6566 3d22 436f 712e 496e 6974 2e4c href="Coq.Init.L
│ │ │ -0000ba20: 6f67 6963 2e68 746d 6c23 6571 5f73 796d ogic.html#eq_sym
│ │ │ -0000ba30: 223e 3c73 7061 6e20 636c 6173 733d 2269 ">
eq_sym A.
. &n
│ │ │ -0000bae0: 6273 703b 266e 6273 703b 266e 6273 703b bsp;
│ │ │ -0000baf0: 3c73 7061 6e20 636c 6173 733d 2269 6422
Global Instance
│ │ │ -0000bb20: 3c2f 7370 616e 3e20 3c61 2069 643d 2265 eq_Transitiv
│ │ │ -0000bb90: 653c 2f73 7061 6e3e 3c2f 613e 203a 203c e : <
│ │ │ -0000bba0: 6120 636c 6173 733d 2269 6472 6566 2220 a class="idref"
│ │ │ -0000bbb0: 6872 6566 3d22 436f 712e 436c 6173 7365 href="Coq.Classe
│ │ │ -0000bbc0: 732e 5265 6c61 7469 6f6e 436c 6173 7365 s.RelationClasse
│ │ │ -0000bbd0: 732e 6874 6d6c 2354 7261 6e73 6974 6976 s.html#Transitiv
│ │ │ -0000bbe0: 6522 3e3c 7370 616e 2063 6c61 7373 3d22 e">
Transitive (@eq A) := @eq_trans A
│ │ │ -0000bdc0: 3c2f 613e 2e3c 6272 2f3e 0a0a 3c62 722f .
..
..Leib
│ │ │ -0000bdf0: 696e 7a20 6571 7561 6c69 7479 203c 7370 inz equality eq is an equiva
│ │ │ -0000be50: 6c65 6e63 6520 7265 6c61 7469 6f6e 2e0a lence relation..
│ │ │ -0000be60: 2020 2020 2020 2020 5468 6520 696e 7374 The inst
│ │ │ -0000be70: 616e 6365 2068 6173 206c 6f77 2070 7269 ance has low pri
│ │ │ -0000be80: 6f72 6974 7920 6173 2069 7420 6973 2061 ority as it is a
│ │ │ -0000be90: 6c77 6179 7320 6170 706c 6963 6162 6c65 lways applicable
│ │ │ -0000bea0: 0a20 2020 2020 2020 2069 6620 6f6e 6c79 . if only
│ │ │ -0000beb0: 2074 6865 2074 7970 6520 6973 2063 6f6e the type is con
│ │ │ -0000bec0: 7374 7261 696e 6564 2e20 0a3c 2f64 6976 strained. .
....L
│ │ │ -0000c1f0: 6569 626e 697a 2064 6973 6571 7561 6c69 eibniz disequali
│ │ │ -0000c200: 7479 2e20 0a3c 2f64 6976 3e0a 3c64 6976 ty. ..
..
.
│ │ │ -0000c2f0: 4469 7365 7175 616c 6974 7920 6973 2073 Disequality is s
│ │ │ -0000c300: 796d 6d65 7472 6963 2e20 0a3c 2f64 6976 ymmetric. ..
..
.We now
│ │ │ -00012ae0: 2064 6576 656c 6f70 2061 2067 656e 6572 develop a gener
│ │ │ -00012af0: 616c 697a 6174 696f 6e20 6f66 2072 6573 alization of res
│ │ │ -00012b00: 756c 7473 206f 6e20 7265 6c61 7469 6f6e ults on relation
│ │ │ -00012b10: 7320 666f 7220 6172 6269 7472 6172 7920 s for arbitrary
│ │ │ -00012b20: 7072 6564 6963 6174 6573 2e0a 2020 2054 predicates.. T
│ │ │ -00012b30: 6865 2072 6573 756c 7469 6e67 2074 6865 he resulting the
│ │ │ -00012b40: 6f72 7920 6361 6e20 6265 2061 7070 6c69 ory can be appli
│ │ │ -00012b50: 6564 2074 6f20 686f 6d6f 6765 6e65 6f75 ed to homogeneou
│ │ │ -00012b60: 7320 6269 6e61 7279 2072 656c 6174 696f s binary relatio
│ │ │ -00012b70: 6e73 2062 7574 2061 6c73 6f20 746f 0a20 ns but also to.
│ │ │ -00012b80: 2020 6172 6269 7472 6172 7920 6e2d 6172 arbitrary n-ar
│ │ │ -00012b90: 7920 7072 6564 6963 6174 6573 2e20 0a3c y predicates. .<
│ │ │ -00012ba0: 2f64 6976 3e0a 3c64 6976 2063 6c61 7373 /div>.
..
.
│ │ │ -00012bc0: 3c73 7061 6e20 636c 6173 733d 2269 6422
Local Open Scope
│ │ │ -00012c20: 203c 7370 616e 2063 6c61 7373 3d22 6964 li
│ │ │ -00012c40: 7374 5f73 636f 7065 3c2f 7370 616e 3e2e st_scope.
│ │ │ -00012c50: 3c62 722f 3e0a 0a3c 6272 2f3e 0a3c 2f64
..
....A compact
│ │ │ -00012c80: 2072 6570 7265 7365 6e74 6174 696f 6e20 representation
│ │ │ -00012c90: 6f66 206e 6f6e 2d64 6570 656e 6465 6e74 of non-dependent
│ │ │ -00012ca0: 2061 7269 7469 6573 2c20 7769 7468 2074 arities, with t
│ │ │ -00012cb0: 6865 2063 6f64 6f6d 6169 6e20 7369 6e67 he codomain sing
│ │ │ -00012cc0: 6c65 642d 6f75 742e 200a 3c2f 6469 763e led-out. .
│ │ │ -00012cd0: 0a3c 6469 7620 636c 6173 733d 2263 6f64 ....We ca
│ │ │ -000139c0: 6e20 6465 6669 6e65 2061 6262 7265 7669 n define abbrevi
│ │ │ -000139d0: 6174 696f 6e73 2066 6f72 206f 7065 7261 ations for opera
│ │ │ -000139e0: 7469 6f6e 2061 6e64 2072 656c 6174 696f tion and relatio
│ │ │ -000139f0: 6e20 7479 7065 7320 6261 7365 6420 6f6e n types based on
│ │ │ -00013a00: 203c 7370 616e 2063 6c61 7373 3d22 696e
arrows. .....We def
│ │ │ -00014720: 696e 6520 6e2d 6172 7920 3c73 7061 6e20 ine n-ary
│ │ │ -00014760: 7072 6564 6963 6174 653c 2f73 7061 6e3e predicate
│ │ │ -00014770: 3c2f 7370 616e 3e73 2061 7320 6675 6e63 s as func
│ │ │ -00014780: 7469 6f6e 7320 696e 746f 203c 7370 616e tions into Prop
│ │ │ -000147d0: 3c2f 7370 616e 3e2e 200a 3c2f 6469 763e . .
│ │ │ -000147e0: 0a3c 6469 7620 636c 6173 733d 2263 6f64 ...
.
Nota
│ │ │ -00014820: 7469 6f6e 3c2f 7370 616e 3e20 3c61 2069 tion predicate l :
│ │ │ -000148c0: 3d20 283c 6120 636c 6173 733d 2269 6472 = (
arrows l <
│ │ │ -00014960: 7370 616e 2063 6c61 7373 3d22 6964 2220 span class="id"
│ │ │ -00014970: 7469 746c 653d 226b 6579 776f 7264 223e title="keyword">
│ │ │ -00014980: 5072 6f70 3c2f 7370 616e 3e29 2e3c 6272 Prop).
..
.
.Unary predic
│ │ │ -000149c0: 6174 6573 2c20 6f72 2073 6574 732e 200a ates, or sets. .
│ │ │ -000149d0: 3c2f 6469 763e 0a3c 6469 7620 636c 6173
....We
│ │ │ -000151c0: 2063 616e 2063 6c6f 7365 2061 2070 7265 can close a pre
│ │ │ -000151d0: 6469 6361 7465 2062 7920 756e 6976 6572 dicate by univer
│ │ │ -000151e0: 7361 6c20 6f72 2065 7869 7374 656e 7469 sal or existenti
│ │ │ -000151f0: 616c 2071 7561 6e74 6966 6963 6174 696f al quantificatio
│ │ │ -00015200: 6e2e 200a 3c2f 6469 763e 0a3c 6469 7620 n. .
....
│ │ │ -000165f0: 506f 696e 7477 6973 6520 6578 7465 6e73 Pointwise extens
│ │ │ -00016600: 696f 6e20 6f66 2061 2062 696e 6172 7920 ion of a binary
│ │ │ -00016610: 6f70 6572 6174 696f 6e20 6f6e 203c 7370 operation on T to a binary o
│ │ │ -00016670: 7065 7261 7469 6f6e 0a20 2020 6f6e 2066 peration. on f
│ │ │ -00016680: 756e 6374 696f 6e73 2077 686f 7365 2063 unctions whose c
│ │ │ -00016690: 6f64 6f6d 6169 6e20 6973 203c 7370 616e odomain is T
│ │ │ -000166e0: 2e0a 2020 2046 6f72 2061 6e20 6f70 6572 .. For an oper
│ │ │ -000166f0: 6174 6f72 206f 6e20 3c73 7061 6e20 636c ator on Prop this lifts
│ │ │ -00016750: 7468 6520 6f70 6572 6174 6f72 2074 6f20 the operator to
│ │ │ -00016760: 6120 6269 6e61 7279 206f 7065 7261 7469 a binary operati
│ │ │ -00016770: 6f6e 2e20 0a3c 2f64 6976 3e0a 3c64 6976 on. ..Poin
│ │ │ -00017660: 7477 6973 6520 6c69 6674 696e 672c 2065 twise lifting, e
│ │ │ -00017670: 7175 6976 616c 656e 7420 746f 2064 6f69 quivalent to doi
│ │ │ -00017680: 6e67 203c 7370 616e 2063 6c61 7373 3d22 ng pointwi
│ │ │ -000176c0: 7365 5f65 7874 656e 7369 6f6e 3c2f 7370 se_extension and c
│ │ │ -000176e0: 6c6f 7369 6e67 2075 7369 6e67 203c 7370 losing using predicate_all
│ │ │ -00017730: 3c2f 7370 616e 3e3c 2f73 7061 6e3e 2e20 .
│ │ │ -00017740: 0a3c 2f64 6976 3e0a 3c64 6976 2063 6c61 .
. ..
│ │ │ +000006d0: 6c61 6235 3031 223e 3c2f 613e 3c68 3120 lab501">