mathlib3

e739cf50 - feat(order_dual): instances for order_dual and shortening proofs (#746)

feat(order_dual): instances for order_dual and shortening proofs (#746) * feat(order_bot): instances for order_bot and shortening proofs * fix(topological_structure); remove unused import