Require Import List Arith.

Definition sorted1 (l:list nat) : Prop :=
  forall l1 l2 x1 x2, l = l1++x1::x2::l2 -> x1 <= x2.

Inductive sorted : list nat -> Prop :=
  s1 : sorted nil
| s2 : forall n, sorted (n::nil)
| s3 : forall n m tl, n <= m -> sorted (m::tl) -> sorted (n::m::tl).

Lemma ss1 : forall l, sorted l -> sorted1 l.
induction 1.
unfold sorted1; intros [ | a tl]; intros; discriminate.
unfold sorted1.
intros [ | a tl] l2 x1 x2 q.
discriminate.
destruct tl; discriminate.
intros l1 l2 x1 x2 q.
destruct l1.
injection q; intros; subst x1 x2; auto.
injection q.
intros q' _; unfold sorted1 in IHsorted.
clear q n0.
apply IHsorted with (1:= q').
Qed.

Lemma s1s : forall l, sorted1 l -> sorted l.
assert (forall l, sorted1 l -> sorted l /\ 
          (forall a, sorted1 (a::l) -> sorted (a::l))).
induction l.
intros _; split; intros; constructor.
intros s1al.
assert (sstail : forall b l, sorted1 (b::l) -> sorted1 l).
unfold sorted1; intros b l' sbl' l1 l2 x1 x2 q.
apply sbl' with (l1 := b::l1) (l2:=l2).
rewrite q; auto.
assert (s1l : sorted1 l) by apply sstail with (1:= s1al).
apply IHl in s1l.
split.
 destruct s1l as [_ H]; auto.
intros b s1bal; constructor.
unfold sorted1 in s1bal; apply s1bal with (l1:=@nil nat)(l2:=l); auto.
destruct s1l as [H' H].
apply H; apply sstail with (1:=s1bal).
intros l s1l; apply H in s1l; destruct s1l; auto.
Qed.

Fixpoint insert (n:nat)(l:list nat) {struct l} : list nat :=
  match l with
    nil => n::nil
  | a::tl => if leb a n then a::insert n tl else n::a::tl
  end.

Lemma insert_unfold :
  forall n l, insert n l = 
  match l with
    nil => n::nil
  | a::tl => if leb a n then a::insert n tl else n::a::tl
  end.
     
Lemma insert_sorted : forall n l, sorted l -> sorted (insert n l).
induction 1.
simpl; constructor.
simpl.
case_eq (leb n0 n); intros leq.
repeat constructor.
apply leb_complete; trivial.
repeat constructor.
apply lt_le_weak; apply leb_complete_conv; trivial.

simpl in IHsorted |- *.
case_eq (leb n0 n); intros leq.
destruct (leb m n).
apply s3; trivial.
apply s3; trivial; apply leb_complete; trivial.
repeat (assumption || constructor).
apply lt_le_weak; apply leb_complete_conv; trivial.
Qed.