nat.S_pred
∀ n, O < n ⇒ ((n-1)+1) = n
Theorem S_pred : forall (n:nat), (lt O n) -> logic.eq (nat) (S (pred n)) n.
theorem S_pred : \forall (n:nat). ((lt) (O) n) -> (eq) (nat) ((S) ((pred) n)) n.
theorem S_pred : forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> (((logic.eq_) (nat.nat)) (((nat.S) ) (((nat.pred_) ) (n)))) (n).
S_pred : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(nat_sttfa.lt(nat_sttfa.sttfa_O)(n) => logic_sttfa_th.eq[nat_sttfa.sttfa_nat](nat_sttfa.sttfa_S(nat_sttfa.pred(n)))(n)))
Printing for OpenTheory is not working at the moment.