matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.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/pnat_pred.ma".
  16 include "ground/arith/pnat_iter.ma".
  17
  18 (* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
  19
  20 definition pminus: pnat → pnat → pnat ≝
  21            λp,q. (ppred^q) p.
  22
  23 interpretation
  24   "minus (positive integers)"
  25   'minus p q = (pminus p q).
  26
  27 (* Basic constructions ******************************************************)
  28
  29 lemma pminus_unit_dx (p): ↓p = p - 𝟏.
  30 // qed.
  31
  32 lemma pminus_succ_dx (p) (q): ↓(p - q) = p - ↑q.
  33 #p #q @(piter_succ … ppred)
  34 qed.
  35
  36 (* Advanced constructions ***************************************************)
  37
  38 lemma pminus_pred_sn (p) (q): ↓(p - q) = ↓p - q.
  39 #p #q @(piter_appl … ppred)
  40 qed.
  41
  42 lemma pminus_unit_sn (q): 𝟏 = 𝟏 - q.
  43 #q elim q -q //
  44 qed.
  45
  46 lemma pminus_succ_bi (p) (q): p - q = ↑p - ↑q.
  47 #p #q elim q -q //
  48 qed.
  49
  50 lemma pminus_succ_dx_pred_sn (p) (q): ↓p - q = p - ↑q.
  51 // qed-.
  52
  53 lemma pminus_refl (p): 𝟏 = p - p.
  54 #p elim p -p //
  55 qed.
  56
  57 lemma pminus_succ_sn_refl (p): 𝟏 = ↑p - p.
  58 #p elim p -p //
  59 qed.
  60
  61 lemma pminus_comm_21 (p) (q1) (q2): p - q1 - q2 = p - q2 - q1.
  62 #p #q1 #q2 elim q2 -q2 //
  63 qed.
  64
  65 lemma pminus_comm_231 (p) (q1) (q2) (q3):
  66       p-q1-q2-q3 = p-q2-q3-q1.
  67 // qed.