matita/matita/contribs/BTM/arith.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/exp.ma".
  16 include "../lambda_delta/ground_2/arith.ma".
  17
  18 lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
  19 #m * /2 width=1/ normalize
  20 #n #H destruct
  21 qed-.
  22
  23 lemma times_inv_S2_O3: ∀m,n. n * (S m) = 0 → n = 0.
  24 #m #n <times_n_Sm #H
  25 elim (plus_inv_O3 … H) -H //
  26 qed-.
  27
  28 lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
  29 // qed.
  30
  31 lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
  32 #n #m >distributive_times_plus_r //
  33 qed.
  34
  35 lemma lt_plus_nmn_false: ∀m,n. n + m < n → False.
  36 #m #n elim n -n
  37 [ #H elim (lt_zero_false … H)
  38 | /3 width=1/
  39 ]
  40 qed-.
  41
  42 lemma not_b_divides_nbr: ∀b,r. 0 < r → r < b →
  43                          ∀n,m. n * b + r = m * b → False.
  44 #b #r #Hr #Hrb #n elim n -n
  45 [ * normalize
  46   [ -Hrb #H destruct elim (lt_refl_false … Hr)
  47   | -Hr #m #H destruct
  48     elim (lt_plus_nmn_false … Hrb)
  49   ]
  50 | #n #IHn * normalize
  51   [ -IHn -Hrb #H destruct
  52     elim (plus_inv_O3 … H) -H #_ #H destruct
  53     elim (lt_refl_false … Hr)
  54   | -Hr -Hrb /3 width=3/
  55   ]
  56 ]
  57 qed-.