From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 28 Sep 2005 10:15:40 +0000 (+0000)
Subject: New entry: relevant_equations.
X-Git-Tag: V_0_7_2_3~286
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c6b8eec9db4119a87eb4fd4055f1ac31a713d90;p=helm.git

New entry: relevant_equations.
---

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 71734fad3..26e3dcc82 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -210,6 +210,15 @@ constructor 1.assumption.
 rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
 qed.
 
+theorem eq_div_O: \forall n,m. n < m \to n / m = O.
+intros.
+apply div_mod_spec_to_eq n m (n/m) (n \mod m) O n.
+apply div_mod_spec_div_mod.
+apply le_to_lt_to_lt O n m.
+apply le_O_n.assumption.
+constructor 1.assumption.reflexivity.
+qed.
+
 theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
 intros.
 apply div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O.
diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index aafdc2f19..5d04a7c81 100644
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/fermat_little_theorem".
 
+include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
 
@@ -88,3 +89,10 @@ apply trans_lt ? (S O).simplify.apply le_n.assumption.
 apply H4.
 qed.
 
+(*
+theorem bad : \forall p,a:nat. prime p \to \lnot divides p a \to
+mod (exp a (pred p)) p = (S O). 
+intros.
+cut map_iter p (\lambda x.x) times (S O) = 
+map_iter p (\lambda n.(mod (a*n) p)) times (S O).
+*)
\ No newline at end of file
diff --git a/helm/matita/library/nat/relevant_equations.ma b/helm/matita/library/nat/relevant_equations.ma
new file mode 100644
index 000000000..fee1fd407
--- /dev/null
+++ b/helm/matita/library/nat/relevant_equations.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       __                                                               *)
+(*      ||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".
+
+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_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.