X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=9494a28d7983b9735d8f04e58d00db58512da77a;hb=03fcee16d9c262aad38a47d0a409b684a965cc3f;hp=5bef2237103f27308663712a78f78b67d0c3b621;hpb=4d6bf14d95252ecfd1aaca4568184b4d6dee9b24;p=helm.git diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index 5bef22371..9494a28d7 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -160,3 +160,4 @@ apply inj_times_r n.assumption. apply lt_to_not_eq.assumption. intro.reflexivity. qed. +