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

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

nat!N_lt_sN : {N:nat} nat_lt N (s_nat N) -> type.
%mode nat!N_lt_sN +N -DNatLt.
-z             : nat!N_lt_sN z_nat (nat_lt_z).
-s             : nat!N_lt_sN (s_nat N) (nat_lt_s DNatLt)
		  <- nat!N_lt_sN N DNatLt.
%terminates N (nat!N_lt_sN N _).
%worlds () (nat!N_lt_sN _ _).
%covers nat!N_lt_sN +N -DNatt.
%total N (nat!N_lt_sN N _).

nat!lt_trans   : nat_lt N1 N2 -> nat_lt N2 N3 -> nat_lt N1 N3 -> type.
%mode nat!lt_trans +DNatLt12 +DNatLt23 -DNatLt13.
-z             : nat!lt_trans nat_lt_z _ nat_lt_z.
-s             : nat!lt_trans (nat_lt_s DNatLt12) 
                              (nat_lt_s DNatLt23) 
                              (nat_lt_s DNatLt13)
		  <- nat!lt_trans DNatLt12 DNatLt23 DNatLt13.
%worlds () (nat!lt_trans _ _ _).
%total DNatLt12 (nat!lt_trans DNatLt12 _ _).

nat!lt_contradict
               : nat_lt N N -> absurd -> type.
%mode nat!lt_contradict +DNatLt -Absurd.
-s             : nat!lt_contradict (nat_lt_s DNatLt) Absurd
		  <- nat!lt_contradict DNatLt Absurd.
%worlds () (nat!lt_contradict _ _).
%total DNatLt (nat!lt_contradict DNatLt _).