Commit 2024-06-19 12:59 c59e5958

chore: replace continuity by fun_prop, easy cases (#13880) Inspired by #12661: let's start with some easy instances, so we can focus on the difficult ones. In particular, this PR does not depend on any in-progress bugfixes, not tries to change a default value by continuity to by fun_prop. I am not at all confident about the tagging of lemmas with fun_prop: I remember this being subtle, but can't find any documentation on this. @lecopivo Can you advise on these lemmas (or simply link to the right documentation if I just overlooked it)?