We present cut-free Gentzen-style sequent calculi for the theories of linearly ordered lattices and of linearly ordered Heyting algebras thereby providing simple solutions to the decision problems for universally quantified formulae in these theories. In addition to rules decomposing zero-order formulae, there are rules to decompose terms built from the algebraic operations. The ideas are related to prior work on lattice theory and on Gödel-Dummett logic.