-(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(match y in nat return
-(\lambda (n0: nat).(le (minus (S n) n0) (S n))) with [O \Rightarrow (le_n (S
-n)) | (S n0) \Rightarrow (le_S (minus n n0) n (H n0))])))) x).
+(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0:
+nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda
+(_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)])
+(S n))).(le_S (minus n n0) n (H n0)))) y)))) x).