Commit 2025-03-12 11:29 7d0d31ed

View on Github →

feat(Data/Nat/Find): Nat.find_mono_of_le and Nat.find_congr (#22811) Both strong versions (p and q agree below some x) and weak (p and q agree everywhere) helper for not juggling generalize_proofs

Estimated changes

added theorem Nat.find_congr'
added theorem Nat.find_congr
modified theorem Nat.find_mono
added theorem Nat.find_mono_of_le