definition lt: nat \to nat \to Prop \def
\lambda n,m:nat.(S n) \leq m.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
definition lt: nat \to nat \to Prop \def
\lambda n,m:nat.(S n) \leq m.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).