mathlib

706a824c - feat(data/{nat, real}/sqrt): Some simple facts about square roots (#12851)

feat(data/{nat, real}/sqrt): Some simple facts about square roots (#12851) Prove that sqrt 1 = 1 in the natural numbers and an order relationship between real and natural square roots. Co-authored-by: Johan Commelin <johan@commelin.net>