Commit 2023-02-24 10:27 634284e7
View on Github →refactor(data/real/ereal): add a two-argument induction principle (#18481)
We use exactly the same induction process whenever proving anything about * on ereal, so we may as well package it into a helper lemma.