proposition: Theorem sorted_cdr : forall (n : nat) (x : list nat), sorted (Cons nat n x) -> sorted x.
proof: Proof. simple induction x. intro. unfold sorted in |- *. trivial. intro. intro. intro. rewrite sorted_eq3. tauto. Qed.