%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% nat-lemmas.thm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Nat Less-than Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%theorem
nat!N_lt_sN_thm : 
          forall {N:nat} 
          exists {DNatLt: nat_lt N (s_nat N)}
          true.
%prove 2 N (nat!N_lt_sN_thm N _).

%theorem
nat!lt_trans_thm :
          forall* {N1:nat} {N2:nat} {N3:nat}
          forall {DNatLt12: nat_lt N1 N2}
                 {DNatLt23: nat_lt N2 N3}
          exists {DNatLt13: nat_lt N1 N3}
          true.
%prove 2 DNatLt12 (nat!lt_trans_thm DNatLt12 _ _).

%theorem
nat!lt_contradict_thm :
          forall* {N:nat}
          forall {DNatLt: nat_lt N N}
          exists {Absurd: absurd}
          true.
%prove 2 DNatLt (nat!lt_contradict_thm DNatLt _).