X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fnat_ordered_set.ma;h=d4aa1d57d18780367e650b63dc9ad37eb0109a72;hb=6d27950e804ea499909ae0fabceea99f35d118e9;hp=18ecf8e6027f7ca5ada1011dfb45825d4fc84b4e;hpb=7af9d84f465b5f4b609b08ae914681526d12480a;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma index 18ecf8e60..d4aa1d57d 100644 --- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "bishop_set.ma". include "nat/compare.ma". -include "cprop_connectives.ma". +include "bishop_set.ma". definition nat_excess : nat → nat → CProp ≝ λn,m. m