\forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
\forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt