Inductive
    lt : nat->nat->Prop :=
	lt_O : (i:nat)(lt O (S i)) |
	lt_S : (i,j:nat)(lt i j)->(lt (S i) (S j)).