Not all relations are transitive, so you're going to need to use the definition of
le, or some lemma that you've already proved about them.
Intuitively speaking, there are two cases: either $m = o'$ or $m \lt o'$. In the first case,
Hnm says that $S(n) \le o'$, from which the conclusion is one application of
le_S away. In the second case, you can apply
This form of reasoning assumes some very well-known facts about arithmetic. (It's usually hard to formally prove something if you don't already have some intuition about the topic.) But you haven't proved them yet, so you can't directly use them. Instead, you have to make these cases appear via the construction of the data or the proof. It's very common to reason about the structure of a proof hypothesis: such-and-such hypothesis is of this form, and therefore it can only have been constructed in a certain way.
An important tactic for reasoning about the structure of a hypotheses in a non-recursive way is
inversion. Roughly speaking,
inversion does case analysis on a hypothesis and works out how these cases can be possible, unlike
destruct which does case analysis but loses information on how the hypothesis could be possible. We want to reason about how $m \le o'$ can be possible, and there's a hypothesis that's very cloes to this:
Hmo. So apply the tactic
I'll let you work out the details of the proof. If you don't care about the details, Coq will fill them in for you, but as a learning exercise you should complete these
auto steps by hand.
Theorem lt_trans'' :
forall n m o, n < m -> m < o -> n < o.
intros n m o Hnm Hmo.
induction o; inversion Hmo; subst; auto.