monotonic le pred

Theorem monotonic_pred : relations.monotonic (nat) le pred.

theorem monotonic_pred : (monotonic) (nat) (le) (pred) .

theorem monotonic_pred : (((relations.monotonic) (nat.nat)) ((nat.le_) )) ((nat.pred_) ).

monotonic_pred : LEMMA relations_sttfa_th.monotonic[nat_sttfa.sttfa_nat](nat_sttfa.le)(nat_sttfa.pred)

Printing for OpenTheory is not working at the moment.