// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

nat.S_pred

Statement

∀ n, O < n ⇒ ((n-1)+1) = n

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem S_pred : forall (n:nat), (lt O n) -> logic.eq (nat) (S (pred n)) n.



Matita-Jumb
Statement

theorem S_pred : \forall (n:nat). ((lt) (O) n) -> (eq) (nat) ((S) ((pred) n)) n.



Lean-jumb
Statement

theorem S_pred : forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> (((logic.eq_) (nat.nat)) (((nat.S) ) (((nat.pred_) ) (n)))) (n).



PVS-jumb

Statement

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)))



OpenTheory

Printing for OpenTheory is not working at the moment.