1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "arithmetics/exp.ma".
16 include "../lambda_delta/ground_2/arith.ma".
18 lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
19 #m * /2 width=1/ normalize
23 lemma times_inv_S2_O3: ∀m,n. n * (S m) = 0 → n = 0.
25 elim (plus_inv_O3 … H) -H //
28 lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
31 lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
32 #n #m >distributive_times_plus_r //
35 lemma lt_plus_nmn_false: ∀m,n. n + m < n → False.
37 [ #H elim (lt_zero_false … H)
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
46 [ -Hrb #H destruct elim (lt_refl_false … Hr)
48 elim (lt_plus_nmn_false … Hrb)
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/