Coq < Inductive Le : nat->nat->Set :=
  LeO : (n:nat)(Le O n) 
| LeS : (n,m:nat) (Le n m)->
                  (Le (S n) (S m)).

Coq < Variable P:nat->nat->Prop.

Coq < Variable Q:(n,m:nat)
                   (Le n m)->Prop.