nat.monotonic_pred
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.