Truncated logarithm over the natural numbers#1311

Open

LorenzoMolena wants to merge 3 commits into

agda:masterfrom

LorenzoMolena:logN

Commits on May 31, 2026

add module `Nat/Logarithm` and missing properties in `Nat/Order`, `Nat/Mod` ; move `≤-·sk-cancel` and `<-·sk-cancel` from `Fin/Properties` to `Nat/Order`, giving shorter inductive proofs
LorenzoMolena
committed

Commits on Jun 1, 2026