]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_minus_plus.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 "ground/arith/nat_plus.ma".
16 include "ground/arith/nat_minus.ma".
17
18 (* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
19
20 (* Constructions with nplus *************************************************)
21
22 (*** minus_plus_m_m *)
23 lemma nminus_plus_sn_refl_sn (m) (n): m = m + n - n.
24 #m #n @(nat_ind_succ … n) -n //
25 #n #IH <nplus_succ_dx <nminus_succ_bi //
26 qed.
27
28 (*** minus_plus_m_m_commutative *)
29 lemma nminus_plus_sn_refl_dx (m) (n): m = n + m - n.
30 #m #n <nplus_comm //
31 qed.
32
33 (*** minus_plus *)
34 theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n).
35 #o #m #n @(nat_ind_succ … n) -n //
36 #n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
37 qed.
38
39 (*** minus_plus_plus_l *)
40 lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
41 #m #n #o <nminus_plus_assoc <nminus_comm //
42 qed.
43
44 (* Helper constructions with nplus ******************************************)
45
46 (*** plus_to_minus *)
47 lemma nminus_plus_dx (o) (m) (n): o = m+n → n = o-m.
48 #o #m #n #H destruct //
49 qed-.
50
51 lemma nminus_plus_sn (o) (m) (n): o = m+n → m = o-n.
52 #o #m #n #H destruct //
53 qed-.
54
55 (* Inversions with nplus ****************************************************)
56
57 (*** discr_plus_xy_minus_xz *)
58 lemma eq_inv_plus_nminus_refl_sn (m) (n) (o):
59       m + o = m - n →
60       ∨∨ ∧∧ 𝟎 = m & 𝟎 = o
61        | ∧∧ 𝟎 = n & 𝟎 = o.
62 #m #n @(nat_ind_2_succ … m n) -m -n
63 [ /3 width=1 by or_introl, conj/
64 | #m #_ #o #Ho
65   lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
66   /3 width=1 by or_intror, conj/
67 | #m #n #IH #o
68   <nminus_succ_bi >nplus_succ_shift #Ho
69   elim (IH … Ho) -IH -Ho * #_ #H
70   elim (eq_inv_zero_nsucc … H)
71 ]
72 qed-.
73
74 (*** discr_minus_x_xy *)
75 lemma eq_inv_nminus_refl_sn (m) (n): m = m - n → ∨∨ 𝟎 = m | 𝟎 = n.
76 #m #n #Hmn
77 elim (eq_inv_plus_nminus_refl_sn … (𝟎) Hmn) -Hmn * #H1 #H2
78 /2 width=1 by or_introl, or_intror/
79 qed-.