(**) (* reverse include *)
include "ground/arith/nat_rplus_pplus.ma".
include "ground/relocation/tr_pn_eq.ma".
include "ground/relocation/tr_compose_pn.ma".
include "ground/relocation/nap.ma".
(**) (* reverse include *)
include "ground/arith/nat_rplus_pplus.ma".
include "ground/relocation/tr_pn_eq.ma".
include "ground/relocation/tr_compose_pn.ma".
include "ground/relocation/nap.ma".