mathlib3

2d3c522b - feat(order/ideal): added proper ideal typeclass and lemmas to order_top (#6566)

feat(order/ideal): added proper ideal typeclass and lemmas to order_top (#6566) Defined `proper` and proved basic lemmas about proper ideals. Also turned `order_top` into a section.