helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma

   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 (* This file was automatically generated: do not edit *********************)
  16
  17 include "preamble.ma".
  18
  19 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con".
  20
  21 inline procedural
  22 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con".
  23
  24 inline procedural
  25 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con".
  26
  27 inline procedural
  28 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con".
  29
  30 inline procedural
  31 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con".
  32
  33 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con".
  34
  35 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con".
  36
  37 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con".
  38
  39 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con".
  40
  41 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con".
  42
  43 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con".
  44
  45 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con".
  46
  47 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con".
  48
  49 inline procedural
  50 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con".
  51
  52 inline procedural
  53 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con".
  54
  55 inline procedural
  56 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con".
  57
  58 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con".
  59
  60 inline procedural
  61 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con".
  62
  63 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con".
  64
  65 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con".
  66
  67 inline procedural
  68 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con".
  69
  70 inline procedural
  71 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con".
  72
  73 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con".
  74
  75 inline procedural
  76 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con".
  77
  78 inline procedural
  79 "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con".
  80
  81 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con".
  82
  83 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con".
  84
  85 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con".
  86
  87 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con".
  88
  89 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con".
  90
  91 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con".
  92
  93 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con".
  94
  95 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con".
  96
  97 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con".
  98
  99 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con".
 100
 101 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con".
 102
 103 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con".
 104
 105 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con".
 106
 107 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con".
 108
 109 inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con".
 110