Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)

I am an instructor at university for a class titled Type Systems of Languages and the professor used the following example for inductive proofs in Type Theory on the board last lecture:

Suppose, that there are natural numbers defined inductively (for some reason he insists on calling them terms) and we have a greater than function defined recursively on them. We can proove that for every n it holds that (suc n > n).

I have the following Coq code prepared for implementing this in a class:

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
  induction t.

  (* zero *)
  - simpl.
    reflexivity.

  (* suc t *)
  -

which takes me to the following goal:

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

I can solve this in multiple ways by rewriting, unfolding, and / or simplifying before it just turns into reflexivity, but what I would really like to do to make it cleaner is to apply one iteration of greaterThan, that would just turn (suc (suc t) > suc t) = true into (suc t > t) = true, and I could finish the proof with exact IHt.

Is there a way to ahieve this?

ps.: I know that I can simpl in IHt and then use exact, but it expands to the match expression which is much more verbose than what is neccessary here.

Edit: Thanks to Théo Winterhalter's answer I realized that I could also use exact by itself, since the terms are convertible, but that wouldn't show the process too well to the students. (Side note: Both cases of the induction are solvable with trivial as well, but I don't think that they would learn too much from that either. :D)

Solution

Another possibility is to use the Arguments vernacular to tell simpl not to reduce greaterThan to a match expression. Put Arguments greaterThan: simpl nomatch. somewhere after the definition of greaterThan. Then when you use simpl in the environment

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

you get

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc t > t) = true

as you wanted.