Require Import List.

Inductive Sorted : list nat -> Prop :=
| Snil : Sorted (nil (A:=nat))
| Sone : forall n, Sorted (cons n nil)
| Scons : forall l n1 n2,  
                Sorted (cons n2 l) -> 
                n1 < n2 -> 
                  Sorted (cons n1 (cons n2 l)).

Goal (forall x, Sorted (x+1::nil)).
apply Sone.
constructor.
Show Proof.

Goal Sorted (1::2::3::nil).
constructor.
constructor.
constructor.
Show Proof.
constructor.
Show Proof.
Locate "<".
Print lt.
Locate "<=".
Print le.


Goal forall a:nat, a<>a \/ a=a.
right.
constructor.



Goal bool.
left.


Print ex.
Locate "exists".

Goal (exists x:nat, x=x).
exists 7.
Show Proof.
split with 7.
constructor 1 with 7.