]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/congruence.ma
- new definition of lazy equivalence for local environments,
[helm.git] / weblib / arithmetics / congruence.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/primes.ma".
13
14 (* successor mod n *)
15 definition S_mod: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
16 λn,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n.
17
18 definition congruent: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
19 λn,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 n p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 m p.
20
21 interpretation "congruent" 'congruent n m p = (congruent n m p).
22
23 notation "hvbox(n break ≅_{p} m)"
24   non associative with precedence 45
25   for @{ 'congruent $n $m $p }.
26   
27 theorem congruent_n_n: ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} n .
28 // qed.
29
30 theorem transitive_congruent: 
31   ∀p.\ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λn,m.\ 5a href="cic:/matita/arithmetics/congruence/congruent.def(4)"\ 6congruent\ 5/a\ 6 n m p).
32 /2/ qed.
33
34 theorem le_to_mod: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m.
35 #n #m #ltnm @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n m \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m))
36 % // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(6)"\ 6ltn_to_ltO\ 5/a\ 6 … ltnm) 
37 qed.
38
39 theorem mod_mod : ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6p → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p.
40 #n #p #posp >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) p) in ⊢ (? ? % ?) 
41 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_O.def(14)"\ 6eq_div_O\ 5/a\ 6 ? p) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
42 qed.
43
44 theorem mod_times_mod : ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6p → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6m → 
45   n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p.
46 #n #m #p #posp #posm
47 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n p (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) 
48 (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p))) 
49   [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 //
50   |% [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //] >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6
51    >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 //
52   ]
53 qed.
54
55 theorem congruent_n_mod_n : ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p →
56  n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p).
57 /2/ qed.
58
59 theorem congruent_n_mod_times : ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → 
60   n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)).
61 /2/ qed.
62
63 theorem eq_times_plus_to_congruent: ∀n,m,p,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → 
64   n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m → n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} m .
65 #n #m #p #r #posp #eqn
66 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n p (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n p) (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 n p) (r \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 m p)) (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 m p))
67   [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 //
68   |% [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //] >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6
69    >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 //
70   ]
71 qed.
72
73 theorem divides_to_congruent: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 n → 
74   p \ 5a title="divides" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6(n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 m) → n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} m .
75 #n #m #p #posp #lemn * #l #eqpl 
76 @(\ 5a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"\ 6eq_times_plus_to_congruent\ 5/a\ 6 … l posp) /2/
77 qed.
78
79 theorem congruent_to_divides: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → 
80   n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} m → p \ 5a title="divides" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 m).
81 #n #m #p #posp #congnm @(\ 5a href="cic:/matita/arithmetics/primes/divides.con(0,1,2)"\ 6quotient\ 5/a\ 6 ? ? ((n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)))
82 >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n p) in ⊢ (??%?)
83 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m p) in ⊢ (??%?) <(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))
84 <congnm <(\ 5a href="cic:/matita/arithmetics/nat/minus_plus.def(12)"\ 6minus_plus\ 5/a\ 6 ? (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)) <\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6 //
85 qed.
86
87 theorem mod_times: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → 
88   n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p).
89 #n #m #p #posp @(\ 5a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"\ 6eq_times_plus_to_congruent\ 5/a\ 6 ?? p 
90   ((n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p))) //
91 @(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ?? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))))
92   [@\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //
93   |@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ? ? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6
94     (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))) //
95    >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"\ 6distributive_times_plus\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 
96    >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //
97   ]
98 qed.
99
100 theorem congruent_times: ∀n,m,n1,m1,p. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p → 
101   n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} n1 → m \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} m1 → n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6_{p} n1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m1 .
102 #n #m #n1 #m1 #p #posp #congn #congm
103 @(\ 5a href="cic:/matita/arithmetics/congruence/transitive_congruent.def(5)"\ 6transitive_congruent\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"\ 6mod_times\ 5/a\ 6 n m p posp))
104 >congn >congm @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"\ 6mod_times\ 5/a\ 6 //
105 qed.
106
107 (*
108 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
109 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
110 intros.
111 elim n. simplify.
112 apply congruent_n_mod_n.assumption.
113 simplify.
114 apply congruent_times.
115 assumption.
116 apply congruent_n_mod_n.assumption.
117 assumption.
118 qed. *)