X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Fnat%2Frelevant_equations.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Frelevant_equations.ma;h=f4cf43775058d9cfdd550c68f2cb959f00fba512;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git diff --git a/helm/matita/library/nat/relevant_equations.ma b/helm/matita/library/nat/relevant_equations.ma new file mode 100644 index 000000000..f4cf43775 --- /dev/null +++ b/helm/matita/library/nat/relevant_equations.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* __ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/relevant_equations.ma". + +include "nat/times.ma". +include "nat/minus.ma". + +theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p. +intros. +apply (trans_eq ? ? (p*(n+m))). +apply sym_times. +apply (trans_eq ? ? (p*n+p*m)). +apply distr_times_plus. +apply eq_f2. +apply sym_times. +apply sym_times. +qed. + +theorem times_minus_l: \forall n,m,p:nat. (n-m)*p = n*p - m*p. +intros. +apply (trans_eq ? ? (p*(n-m))). +apply sym_times. +apply (trans_eq ? ? (p*n-p*m)). +apply distr_times_minus. +apply eq_f2. +apply sym_times. +apply sym_times. +qed. + +theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) = +n*p + n*q + m*p + m*q. +intros. +apply (trans_eq nat ? ((n*(p+q) + m*(p+q)))). +apply times_plus_l. +rewrite > distr_times_plus. +rewrite > distr_times_plus. +rewrite < assoc_plus.reflexivity. +qed.