∀ a x n, a < ((a + x) + (n+1))

Theorem lt_plus_Sn_r : forall (a:nat), forall (x:nat), forall (n:nat), lt a (plus (plus a x) (S n)).

theorem lt_plus_Sn_r : \forall (a:nat). \forall (x:nat). \forall (n:nat). (lt) a ((plus) ((plus) a x) ((S) n)).

theorem lt_plus_Sn_r : forall (a:nat.nat) , forall (x:nat.nat) , forall (n:nat.nat) , (((nat.lt_) ) (a)) ((((nat.plus) ) ((((nat.plus) ) (a)) (x))) (((nat.S) ) (n))).

lt_plus_Sn_r : LEMMA (FORALL(a:nat_sttfa.sttfa_nat):(FORALL(x:nat_sttfa.sttfa_nat):(FORALL(n:nat_sttfa.sttfa_nat):nat_sttfa.lt(a)(nat_sttfa.plus(nat_sttfa.plus(a)(x))(nat_sttfa.sttfa_S(n))))))

Printing for OpenTheory is not working at the moment.