]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/div_and_mod.ma
- new definition of lazy equivalence for local environments,
[helm.git] / weblib / arithmetics / div_and_mod.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/nat.ma".
13
14 \ 5img class="anchor" src="icons/tick.png" id="mod_aux"\ 6let rec mod_aux p m n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
15 match p with
16   [ O ⇒ m
17   | S q ⇒ match (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n) with
18     [ true ⇒ m
19     | false ⇒ mod_aux q (m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) n]].
20
21 \ 5img class="anchor" src="icons/tick.png" id="mod"\ 6definition 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 ≝
22 λn,m. match m with 
23   [ O ⇒ n
24   | S p ⇒ \ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 n n p]. 
25
26 interpretation "natural remainder" 'module x y = (mod x y).
27
28 \ 5img class="anchor" src="icons/tick.png" id="div_aux"\ 6let rec div_aux p m n : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
29 match p with
30   [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
31   | S q ⇒ match (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n) with
32     [ true ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
33     | false ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (div_aux q (m\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) n)]].
34
35 \ 5img class="anchor" src="icons/tick.png" id="div"\ 6definition div : \ 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 ≝
36 λn,m.match m with 
37   [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n
38   | S p ⇒ \ 5a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"\ 6div_aux\ 5/a\ 6 n n p]. 
39
40 interpretation "natural divide" 'divide x y = (div x y).
41
42 \ 5img class="anchor" src="icons/tick.png" id="le_mod_aux_m_m"\ 6theorem le_mod_aux_m_m: 
43 ∀p,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 p → \ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 p n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 m.
44 #p (elim p)
45 [ normalize #n #m #lenO @(\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"\ 6le_n_O_elim\ 5/a\ 6 …lenO) //
46 | #q #Hind #n #m #len normalize 
47     @(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 n m) normalize //
48     #notlenm @Hind @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"\ 6le_plus_to_minus\ 5/a\ 6
49     @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … len) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
50 qed.
51
52 \ 5img class="anchor" src="icons/tick.png" id="lt_mod_m_m"\ 6theorem lt_mod_m_m: ∀n,m. \ 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 → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m  \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m.
53 #n #m (cases m) 
54   [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
55   |#p #_ normalize @\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/le_mod_aux_m_m.def(11)"\ 6le_mod_aux_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6
56   ]
57 qed.
58
59 \ 5img class="anchor" src="icons/tick.png" id="div_aux_mod_aux"\ 6theorem div_aux_mod_aux: ∀p,n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6
60 n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_aux.fix(0,0,2)"\ 6div_aux\ 5/a\ 6 p n m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod_aux.fix(0,0,2)"\ 6mod_aux\ 5/a\ 6 p n m).
61 #p (elim p)
62   [#n #m normalize //
63   |#q #Hind #n #m normalize
64      @(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 n m) #lenm normalize //
65      >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <(Hind (n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) m)
66      applyS \ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 (* bello *) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
67 qed.
68
69 \ 5img class="anchor" src="icons/tick.png" id="div_mod"\ 6theorem div_mod: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(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\ 6m\ 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).
70 #n #m (cases m) normalize //
71 qed.
72
73 \ 5img class="anchor" src="icons/tick.png" id="eq_times_div_minus_mod"\ 6theorem eq_times_div_minus_mod:
74 ∀a,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (a \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 b) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (a \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b).
75 #a #b (applyS \ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6) qed.
76
77 \ 5img class="anchor" src="icons/tick.png" id="div_mod_spec"\ 6inductive div_mod_spec (n,m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : Prop ≝
78 div_mod_spec_intro: r \ 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\ 6q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r → div_mod_spec n m q r.
79
80 \ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_not_eq_O"\ 6theorem div_mod_spec_to_not_eq_O: 
81   ∀n,m,q,r.\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 n m q r → m \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
82 #n #m #q #r * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6
83 qed.
84
85 \ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_div_mod"\ 6theorem div_mod_spec_div_mod: 
86   ∀n,m. \ 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 → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 n m (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m).
87 #n #m #posm % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
88
89 \ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq"\ 6theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1.
90 \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q r → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q1 r1 → q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q1.
91 #a #b #q #r #q1 #r1 * #ltrb #spec *  #ltr1b #spec1
92 @(\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"\ 6leb_elim\ 5/a\ 6 q q1) #leqq1
93   [(elim (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … leqq1)) //
94      #ltqq1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"\ 6not_le_Sn_n\ 5/a\ 6 a))
95      @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) ?)
96       [>spec (applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"\ 6monotonic_lt_plus_r\ 5/a\ 6 … ltrb))
97       |@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (q1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
98       ]
99   (* this case is symmetric *)
100   |@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_n.def(6)"\ 6not_le_Sn_n\ 5/a\ 6 a))
101      @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q1)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) ?)
102       [>spec1 (applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_r.def(9)"\ 6monotonic_lt_plus_r\ 5/a\ 6 … ltr1b))
103       |cut (q1 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 q) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] #ltq1q @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
104       ]
105   ]
106 qed.
107
108 \ 5img class="anchor" src="icons/tick.png" id="div_mod_spec_to_eq2"\ 6theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1.
109   \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q r → \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.ind(1,0,4)"\ 6div_mod_spec\ 5/a\ 6 a b q1 r1 → r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r1.
110 #a #b #q #r #q1 #r1 #spec #spec1
111 cut (q\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6q1) [@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … spec spec1)] 
112 #eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1 
113 @(\ 5a href="cic:/matita/arithmetics/nat/injective_plus_r.def(5)"\ 6injective_plus_r\ 5/a\ 6 (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b)) //
114 qed.
115
116 \ 5img class="anchor" src="icons/tick.png" id="div_plus_times"\ 6lemma div_plus_times: ∀m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. r \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q.
117 #m #q #r #ltrm
118 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 ???)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
119 qed.
120
121 \ 5img class="anchor" src="icons/tick.png" id="mod_plus_times"\ 6lemma mod_plus_times: ∀m,q,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. r \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (q\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6r) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r. 
122 #m #q #r #ltrm
123 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 ???)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
124 qed.
125
126 (* some properties of div and mod *)
127 \ 5img class="anchor" src="icons/tick.png" id="div_times"\ 6theorem div_times: ∀a,b:\ 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 b → a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
128 #a #b #posb 
129 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6b) b … \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
130 // @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 // qed.
131
132 \ 5img class="anchor" src="icons/tick.png" id="div_n_n"\ 6theorem div_n_n: ∀n:\ 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 n → n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
133 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
134
135 \ 5img class="anchor" src="icons/tick.png" id="eq_div_O"\ 6theorem eq_div_O: ∀n,m. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
136 #n #m #ltnm 
137 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 n m (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) … n (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
138 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
139
140 \ 5img class="anchor" src="icons/tick.png" id="mod_n_n"\ 6theorem mod_n_n: ∀n:\ 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 n → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
141 #n #posn 
142 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n n … \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
143 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
144
145 \ 5img class="anchor" src="icons/tick.png" id="mod_S"\ 6theorem mod_S: ∀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,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → 
146 ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m).
147 #n #m #posm #H 
148 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) m … (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m) ? (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
149 // @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6// (applyS \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6) //
150 qed.
151
152 \ 5img class="anchor" src="icons/tick.png" id="mod_O_n"\ 6theorem mod_O_n: ∀n:\ 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 remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
153 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
154
155 \ 5img class="anchor" src="icons/tick.png" id="lt_to_eq_mod"\ 6theorem lt_to_eq_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="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
156 #n #m #ltnm 
157 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n m (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) … \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …))
158 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"\ 6ltn_to_ltO\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
159
160 (*
161 theorem mod_1: ∀n:nat. mod n 1 = O.
162 #n @sym_eq @le_n_O_to_eq
163 @le_S_S_to_le /2/ qed.
164
165 theorem div_1: ∀n:nat. div n 1 = n.
166 #n @sym_eq napplyS (div_mod n 1) qed. *)
167
168 \ 5img class="anchor" src="icons/tick.png" id="or_div_mod"\ 6theorem or_div_mod: ∀n,q. \ 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 q →
169   ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6q) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n q)) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 q \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
170   ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6q) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n q) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 q \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))).
171 #n #q #posq 
172 (elim (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 ?? (\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 n q posq))) #H
173   [%2 % // (applyS \ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6) //
174   |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)); @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6//
175   ]
176 qed.
177
178 (* injectivity *)
179 \ 5img class="anchor" src="icons/tick.png" id="injective_times_r"\ 6theorem injective_times_r: 
180   ∀n:\ 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 n → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 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 (λm:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m).
181 #n #posn #a #b #eqn 
182 <(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 a n posn) <(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 b n posn) // 
183 qed.
184
185 \ 5img class="anchor" src="icons/tick.png" id="injective_times_l"\ 6theorem injective_times_l: 
186     ∀n:\ 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 n → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 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 (λm:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n).
187 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/injective_times_r.def(15)"\ 6injective_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
188
189 (* n_divides computes the pair (div,mod) 
190 (* p is just an upper bound, acc is an accumulator *)
191 let rec n_divides_aux p n m acc \def
192   match n \mod m with
193   [ O \Rightarrow 
194     match p with
195       [ O \Rightarrow pair nat nat acc n
196       | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
197   | (S a) \Rightarrow pair nat nat acc n].
198
199 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
200 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
201
202 (* inequalities *)
203
204 \ 5img class="anchor" src="icons/tick.png" id="lt_div_S"\ 6theorem lt_div_S: ∀n,m. \ 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 → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(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\ 6m.
205 #n #m #posm (change with (n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m \ 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\ 6m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m))
206 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n m) in ⊢ (? % ?); >\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 
207 @\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 // 
208 qed.
209
210 \ 5img class="anchor" src="icons/tick.png" id="le_div"\ 6theorem le_div: ∀n,m. \ 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 n → m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 m.
211 #n #m #posn
212 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m n) in ⊢ (? ? %); @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
213 qed.
214
215 \ 5img class="anchor" src="icons/tick.png" id="le_plus_mod"\ 6theorem le_plus_mod: ∀m,n,q. \ 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 q →
216 (m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 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 q .
217 #m #n #q #posq
218 (elim (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 q (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 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 q))) #Hle
219   [@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … Hle) @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
220   |cut ((m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n)\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q) //
221      @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 … (m\ 5a title="natural divide" 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 divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q) ? (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 … posq)).
222      @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6
223       [@\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //
224       |>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n q) in ⊢ (? ? (? ? %) ?);
225        (applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (λx.\ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6 x (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))))
226        >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m q) in ⊢ (? ? (? % ?) ?);       
227        (applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 … (λx.\ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6 x (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)))) //
228       ]
229   ]
230 qed.
231
232 \ 5img class="anchor" src="icons/tick.png" id="le_plus_div"\ 6theorem le_plus_div: ∀m,n,q. \ 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 q →
233   m\ 5a title="natural divide" 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 divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\le\ 5/a\ 6 (m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6q.
234 #m #n #q #posq @(\ 5a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"\ 6le_times_to_le\ 5/a\ 6 … posq)
235 @(\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"\ 6le_plus_to_le_r\ 5/a\ 6 ((m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q))
236 (* bruttino *)
237 >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 in ⊢ (? ? %); <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6
238 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m q) in ⊢ (? ? (? % ?)); >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n q) in ⊢ (? ? (? ? %));
239 >\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 in ⊢ (? ? (? % ?)); >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 in ⊢ (? ? %);
240 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 in ⊢ (? ? (? ? %)); (applyS \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/le_plus_mod.def(14)"\ 6le_plus_mod\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
241 qed.
242
243 \ 5img class="anchor" src="icons/tick.png" id="le_times_to_le_div"\ 6theorem le_times_to_le_div: ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6
244   \ 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 b → b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a → c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b.
245 #a #b #c #posb #Hle
246 @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 b) @(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? a)/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"\ 6lt_div_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
247 qed.
248
249 \ 5img class="anchor" src="icons/tick.png" id="le_times_to_le_div2"\ 6theorem le_times_to_le_div2: ∀m,n,q. \ 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 q → 
250   n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q → n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 m.
251 #m #n #q #posq #Hle
252 @(\ 5a href="cic:/matita/arithmetics/nat/le_times_to_le.def(9)"\ 6le_times_to_le\ 5/a\ 6 q ? ? posq) @(\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"\ 6le_plus_to_le\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_a.def(8)"\ 6le_plus_a\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
253 qed.
254
255 (* da spostare 
256 theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m.
257 /2/ qed. *)
258    
259 \ 5img class="anchor" src="icons/tick.png" id="lt_times_to_lt_div"\ 6theorem lt_times_to_lt_div: ∀m,n,q. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q → n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m.
260 #m #n #q #Hlt
261 @(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 q …) @(\ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"\ 6lt_plus_to_lt_l\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 q)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
262 qed.
263
264 (*
265 theorem lt_div: ∀n,m. O < m → 1 < n → m/n < m.
266 #n #m #posm #lt1n
267 @lt_times_to_lt_div (applyS lt_m_nm) //.
268 qed. 
269   
270 theorem le_div_plus_S: ∀m,n,q. O < q →
271 (m+n)/q \le S(m/q + n/q).
272 #m #n #q #posq
273 @le_S_S_to_le @lt_times_to_lt_div
274 @(lt_to_le_to_lt … (lt_plus … (lt_div_S m … posq) (lt_div_S n … posq)))
275 //
276 qed. *)
277
278 \ 5img class="anchor" src="icons/tick.png" id="le_div_S_S_div"\ 6theorem le_div_S_S_div: ∀n,m. \ 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 → (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m).
279 #n #m #posm @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div2.def(10)"\ 6le_times_to_le_div2\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_div_S.def(13)"\ 6lt_div_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
280 qed.
281
282 \ 5img class="anchor" src="icons/tick.png" id="le_times_div_div_times"\ 6theorem le_times_div_div_times: ∀a,n,m.\ 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 → 
283 a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m. 
284 #a #n #m #posm @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"\ 6le_times_to_le_div\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
285 qed.
286
287 \ 5img class="anchor" src="icons/tick.png" id="monotonic_div"\ 6theorem monotonic_div: ∀n.\ 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 n →
288   \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6 (λm.\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 m n).
289 #n #posn #a #b #leab @\ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_to_le_div.def(14)"\ 6le_times_to_le_div\ 5/a\ 6/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
290 qed.
291
292 \ 5img class="anchor" src="icons/tick.png" id="pos_div"\ 6theorem pos_div: ∀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,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 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 n → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 → 
293   \ 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 n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m.
294 #n #m #posm #posn #mod0
295 @(\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"\ 6lt_times_n_to_lt_l\ 5/a\ 6 m)// (* MITICO *)
296 qed.
297
298 (*
299 theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n.
300 #n #m #ltm #posn
301 @(leb_elim 1 (n / m))/2/ (* MITICO *)
302 qed. *)
303
304 \ 5img class="anchor" src="icons/tick.png" id="eq_div_div_div_times"\ 6theorem eq_div_div_div_times: ∀n,m,q. \ 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 n → \ 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 →
305  q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m).
306 #n #m #q #posn #posm
307 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (q\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)) … (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 …)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_times.def(13)"\ 6lt_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
308 @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 // @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m))))
309   [(applyS \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
310   |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
311   ]
312 qed.
313
314 \ 5img class="anchor" src="icons/tick.png" id="eq_div_div_div_div"\ 6theorem eq_div_div_div_div: ∀n,m,q. \ 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 n → \ 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 →
315 q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n.
316 #n #m #q #posn #posm
317 @(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ? ? (q\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m)))
318   [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
319   |@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 (applyS \ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6) //
320   ]
321 qed.
322
323 \ 5img class="anchor" src="icons/tick.png" id="lt_to_le_times_to_lt_S_to_div"\ 6theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
324 \ 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 b → (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 c)) → a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c.
325 #a #c #b #posb#lea #lta
326 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq.def(10)"\ 6div_mod_spec_to_eq\ 5/a\ 6 … (a\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 … posb …))
327 @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6 [@\ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(11)"\ 6lt_plus_to_minus\ 5/a\ 6 // |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"\ 6plus_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
328 qed.
329
330 \ 5img class="anchor" src="icons/tick.png" id="div_times_times"\ 6theorem div_times_times: ∀a,b,c:\ 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 c → \ 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 b → 
331   (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c).
332 #a #b #c #posc #posb
333 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 b) <\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_times.def(14)"\ 6eq_div_div_div_times\ 5/a\ 6 //
334 >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 //
335 qed.
336
337 \ 5img class="anchor" src="icons/tick.png" id="times_mod"\ 6theorem times_mod: ∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
338 \ 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 c → \ 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 b → (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(a\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b).
339 #a #b #c #posc #posb
340 @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(11)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 (a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) ((a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)) (a\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6b) (c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(a \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 b)))
341   [>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times_times.def(15)"\ 6div_times_times\ 5/a\ 6 … posc) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_times.def(13)"\ 6lt_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
342   |@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec.con(0,1,4)"\ 6div_mod_spec_intro\ 5/a\ 6
343     [applyS (\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"\ 6monotonic_lt_times_r\ 5/a\ 6 … c posc) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
344     |(applyS (\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 …(λx.x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c))) //
345     ]
346   ]
347 qed.
348
349 \ 5img class="anchor" src="icons/tick.png" id="le_div_times_m"\ 6theorem le_div_times_m: ∀a,i,m. \ 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 i → \ 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 →
350  (a \ 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 i)) \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 i.
351 #a #i #m #posi #posm
352 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((a\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6i)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m))
353   [@\ 5a href="cic:/matita/arithmetics/div_and_mod/monotonic_div.def(15)"\ 6monotonic_div\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/div_and_mod/le_times_div_div_times.def(15)"\ 6le_times_div_div_times\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
354   |>\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_div_div_div.def(15)"\ 6eq_div_div_div_div\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/div_and_mod/div_times.def(14)"\ 6div_times\ 5/a\ 6 //
355   ]
356 qed.