From df9feb8fadb3b35ddc8bd899234d8a0320d29a17 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 16 Mar 2009 12:39:54 +0000 Subject: [PATCH] Added a property. --- helm/software/matita/library/nat/times.ma | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 57dc60c6f..32fbc7651 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -21,6 +21,11 @@ let rec times n m \def interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y). +theorem times_Sn_m: +\forall n,m:nat. m+n*m = S n*m. +intros. reflexivity. +qed. + theorem times_n_O: \forall n:nat. O = n*O. intros.elim n. simplify.reflexivity. @@ -90,6 +95,7 @@ theorem symmetric_times : symmetric nat times. unfold symmetric. intros.elim x. simplify.apply times_n_O. +(* applyS times_n_Sm. *) simplify.rewrite > H.apply times_n_Sm. qed. @@ -109,8 +115,9 @@ variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p \def distributive_times_plus. theorem associative_times: associative nat times. -unfold associative.intros. -elim x.simplify.apply refl_eq. +unfold associative. +intros. +elim x. simplify.apply refl_eq. simplify.rewrite < sym_times. rewrite > distr_times_plus. rewrite < sym_times. @@ -120,3 +127,8 @@ qed. variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def associative_times. + +lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). +intros.autobatch paramodulation. +qed. + -- 2.39.2