Theorem eq_le_trans

Proof
01. 1 ⊢ a = b, hypo.
02. 2 ⊢ b ≤ c, hypo.
03. 1, 2 ⊢ a ≤ c, eq_subst_rev 1 2, P t ↔ t ≤ c.
eq_le_trans. ⊢ a = b → b ≤ c → a ≤ c, subj_intro_ii 3.

Dependencies
The given proof depends on two axioms:
eq_refl, eq_subst.