weblib/arithmetics/congruence.ma

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