[elim H13;apply lt_to_le;assumption
|apply in_list_head]]
|apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
|elim (H2 p);elim (H9 H8);split
[assumption
|intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
[elim H13;apply lt_to_le;assumption
|apply in_list_head]]
|apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
|elim (H2 p);elim (H9 H8);split
[assumption
|intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]