From 2263402001ffa3f40e250b736790d93f962685a6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 28 Sep 2005 07:29:39 +0000 Subject: [PATCH] spotted missing times notation --- helm/matita/library/nat/times.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma index 876dfecce..8c53a56c8 100644 --- a/helm/matita/library/nat/times.ma +++ b/helm/matita/library/nat/times.ma @@ -43,7 +43,7 @@ reflexivity. apply assoc_plus. qed. -theorem times_n_SO : \forall n:nat. eq nat n (times n (S O)). +theorem times_n_SO : \forall n:nat. n = n * S O. intros. rewrite < times_n_Sm. rewrite < times_n_O. -- 2.39.2