mathlib3

refactor(order/conditionally_complete_lattice): refactor definition, add constructors

#8496

Open