X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod.ma;h=73344c7c46b0cf1466b0aea949755ced792fc13a;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=ad74a324db86b807cce2bbccc166c8a719fa83d2;hpb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index ad74a324d..73344c7c4 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -133,7 +133,6 @@ rewrite < sym_plus. apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. -(* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *) rewrite > plus_minus. rewrite > sym_times. rewrite < H5.