observational equality of rationals and addition on reals

[blu-bird]

first contribution in a while!

• added a new file for equality of rational numbers in analogy to integers/natural numbers, showed decidability and that equality in $$\mathbb Q$$ is a proposition
• partially defined addition on the reals following the HoTT book (section 11.2.1), details need to be filled in

[VojtechStep]

Hi Bryan, welcome back!

details need to be filled in

Do you plan on filling in the details in this PR? If so, then this PR should be marked as a draft, so that reviewers don't review in-progress work.

[blu-bird]

Converted to a draft! The equality on rationals is mostly done, but I'll unmark it as a draft once the definition is at least filled in.

[fredrik-bakke]

@blu-bird Your work on addition of reals is subsumed by work done by @lowasser in #1307 #1309 #1314, and Egbert is doing a huge refactoring job on the elementary-number-theory module, so it would be good to have just your work on equality of rationals merged. I understand if you're not prioritizing wrapping up this PR at the moment, but could I then take it over from here so it can be merged?