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