mathlib3

0fd51b1c - feat(data/real/irrational): exists irrational between any two distinct rationals and reals (#8753)

feat(data/real/irrational): exists irrational between any two distinct rationals and reals (#8753) Did not find these proofs in `data/real/irrational`, seemed like they belong here. Just proving the standard facts about irrationals between rats and reals. I am using these lemmas in a repo about the Thomae's function.