∀ n m, O < n ⇒ O < (n ^ m)

Theorem lt_O_exp : forall (n:nat.nat), forall (m:nat.nat), (nat.lt nat.O n) -> nat.lt nat.O (exp n m).

theorem lt_O_exp : \forall (n:nat). \forall (m:nat). ((lt) (O) n) -> (lt) (O) ((exp) n m).

theorem lt_O_exp : forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> (((nat.lt_) ) ((nat.O) )) ((((exp.exp) ) (n)) (m)).

lt_O_exp : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(exp_sttfa.sttfa_exp(n)(m)))))

Printing for OpenTheory is not working at the moment.