Constructive order theory puzzle! Prove that every strong total order is decidable (and conversely every decidable total order is strong), with the following definitions:
A partial order is a binary relation that is reflexive, transitive and antisymmetric.A total order is a partial order in which ∀ x y. ∥ (x ≤ y) + (y ≤ x) ∥.A strong total order is a partial order in which ∥ ∀ x y. (x ≤ y) + (y ≤ x) ∥ (hence a total order).An order is decidable if ∀ x y. (x ≤ y) + ¬(x ≤ y).