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\ 6b \ 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\ 6n \ 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\ 6q \ 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\ 6q \ 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 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\ 6c \ 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\ 6q \ 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\ 6q \ 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\ 6m \ 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\ 6m \ 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\ 6m \ 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\ 6b \ 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.