:- module(_, [], [rtchecks_shallow,
	assertions,regtypes,fsyntax,nativeprops,predefres(res_steps)]).


:- prop sorted/1.
sorted([]).
sorted([_]):-!.
sorted([X|T]):-
	X=< ~head(T),
	sorted(T).

head([X|_],X).

:- pred oins(E,L,NL):(num(E),sorted(L),var(NL)) => (num(E),sorted(L),sorted(NL)).
oins(X,[],[X]).
oins(X,[Y|T],[X,Y|T]):-
	X =< Y.
oins(X,[Y|T],[Y|TT]):-
	X > Y,
	oins(X,T,TT).