title: Sorted List in Coq
body: <p>I define a sorted list as follows:</p>
  
  <pre><code>Require Import Coq.Lists.List.
  Import ListNotations.
  
  Inductive SortedList : list nat -&gt; Prop :=
  | sort0 : SortedList []
  | sort1 : forall a, SortedList [a]
  | sort2 : forall z1 z2 l, z1 &lt;= z2 -&gt; SortedList (z2 :: l) -&gt; SortedList (z1 :: z2 :: l).
  </code></pre>
  
  <p>And I think the following theorem is correct.</p>
  
  <pre><code>Theorem SortedList_sep:
    forall l1 l2,
    SortedList (l1 ++ l2) -&gt; SortedList l1 /\ SortedList l2.
  </code></pre>
  
  <p>But I cannot prove this theorem. Can anyone give me some idea?</p>