How can we bring the previously proven theorem in the current frame

[jaewooklee93]

I'm currently studying Rel.v, and meet the case like below.

Hnm : S n <= S m
Hmo : S m <= S o'
______________________________________(1/1)
S n <= S o'

Fortunately, I already prove the following theorem.

Theorem le_trans :
  transitive le.

However, I cannot directly apply this theorem to my goal with apply le_trans, because transitive is not unfolded yet. If I can bring that theorem in my frame, I can unfold it, but I don't know how to do it elegantly. Of course, I can do it as follows, but I have to re-type the statement of the theorem. I guess that there is an easier keyword for doing this.

assert (H:transitive le).
apply le_trans.
unfold transitive in H.
apply H with (b:=S m).

[jaewooklee93]

Um.. I just accidently found that the above 4 lines can be replaced by apply le_trans with (S m). Coq did it quite smart, but I can't understand its mechanism..

[jaewooklee93]

Ah, I understand, Coq just backtracked the definition of transitivity and inferred that it needs only one more missing argument of transitivity, which is (b:=(S m)) in the middle of a<=b<=c.

[jeehoonkang]

:-) @jaewooklee93 your understanding is quite right.

Jeehoon