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 "ground/arith/nat_pred_succ.ma".
16 include "ground/arith/nat_plus.ma".
18 (* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
20 (* Inversions with npred ****************************************************)
22 (*** plus_inv_S3_sn *)
23 lemma eq_inv_succ_nplus_sn (o) (m) (n):
26 | ∧∧ m = ↑↓m & o = ↓m + n.
27 #o #m @(nat_ind_succ … m) -m
28 [ /3 width=1 by or_introl, conj/
29 | #m #_ #n <nplus_succ_sn
30 /4 width=1 by eq_inv_nsucc_bi, or_intror, conj/
34 (*** plus_inv_S3_dx *)
35 lemma eq_inv_succ_nplus_dx (o) (m) (n):
38 | ∧∧ n = ↑↓n & o = m + ↓n.
39 #o #m #n @(nat_ind_succ … n) -n
40 [ /3 width=1 by or_introl, conj/
41 | #n #_ <nplus_succ_sn
42 /4 width=1 by eq_inv_nsucc_bi, or_intror, conj/