include "ground/arith/nat_le_minus_plus.ma".
include "ground/arith/nat_lt.ma".
(* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)
include "ground/arith/nat_le_minus_plus.ma".
include "ground/arith/nat_lt.ma".
(* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)