interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
definition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
definition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.