mathlib

634284e7 - refactor(data/real/ereal): add a two-argument induction principle (#18481)

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. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>