Added a new contrib div_and_mod and few modifs here and there.

[helm.git] / helm / matita / library / nat / orders_op.ma

diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index 801e123d2c901a65c7894c04fe71c9e5920700f6..32a58115dab3dececccbc1eb98fcf9ea431f1ad4 100644 (file)
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -90,7 +90,7 @@ apply le_times_l.assumption.
 apply le_times_r.assumption.
 qed.
 
-theorem le_n_nm: \forall n,m:nat.le (S O) n \to le m (times n m).
+theorem le_times_n: \forall n,m:nat.le (S O) n \to le m (times n m).
 intros.elim H.simplify.
 elim (plus_n_O ?).apply le_n.
 simplify.rewrite < sym_plus.apply le_plus_n.