feat(data/real/cau_seq): more lemmas about sup and inf (#16553)
feat(data/real/cau_seq): more lemmas about sup and inf (#16553)

These will be needed to provide `distrib_lattice real` in terms of these operators later.







leanprover-community/mathlib,leanprover-community/mathlib