X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=f5847033ab0305660fff7faa26f2a2852811e41f;hb=b3f75a04f7516037a1c3dc0735ed17720663356c;hp=8da13d9ab08e7fdbb4d7f165e75394eb69af15b4;hpb=bba3b7f83610c3babb797e8ce1e844a560303295;p=helm.git diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 8da13d9ab..f5847033a 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -280,7 +280,7 @@ rewrite > lt_O_to_div_times assumption |apply lt_exp_Sn_n_SSSO ] - |apply (O_lt_times_to_O_lt ? n2). + |apply (O_lt_times_to_O_lt ? n1). rewrite < H2. assumption ]