helm/software/matita/contribs/procedural/Coq/ZArith/Zhints.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 "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Zhints.v,v 1.8.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
  34
  35 (*#* This file centralizes the lemmas about [Z], classifying them
  36     according to the way they can be used in automatic search  *)
  37
  38 (*i*)
  39
  40 (* Lemmas which clearly leads to simplification during proof search are *)
  41
  42 (* declared as Hints. A definite status (Hint or not) for the other lemmas *)
  43
  44 (* remains to be given *)
  45
  46 (* Structure of the file *)
  47
  48 (* - simplification lemmas (only those are declared as Hints) *)
  49
  50 (* - reversible lemmas relating operators *)
  51
  52 (* - useful Bottom-up lemmas              *)
  53
  54 (* - irreversible lemmas with meta-variables *)
  55
  56 (* - unclear or too specific lemmas       *)
  57
  58 (* - lemmas to be used as rewrite rules   *)
  59
  60 (* Lemmas involving positive and compare are not taken into account *)
  61
  62 include "ZArith/BinInt.ma".
  63
  64 include "ZArith/Zorder.ma".
  65
  66 include "ZArith/Zmin.ma".
  67
  68 include "ZArith/Zabs.ma".
  69
  70 include "ZArith/Zcompare.ma".
  71
  72 include "ZArith/Znat.ma".
  73
  74 include "ZArith/auxiliary.ma".
  75
  76 include "ZArith/Zmisc.ma".
  77
  78 include "ZArith/Wf_Z.ma".
  79
  80 (*#*********************************************************************)
  81
  82 (*                  Simplification lemmas                             *)
  83
  84 (* No subgoal or smaller subgoals                                     *)
  85
  86 (* UNEXPORTED
  87 Hint Resolve
  88   (* A) Reversible simplification lemmas (no loss of information)      *)
  89   (* Should clearly declared as hints                                  *)
  90
  91   (* Lemmas ending by eq *)
  92   Zsucc_eq_compat (* :(n,m:Z)`n = m`->`(Zs n) = (Zs m)` *)
  93
  94   (* Lemmas ending by Zgt *)
  95   Zsucc_gt_compat (* :(n,m:Z)`m > n`->`(Zs m) > (Zs n)` *)
  96   Zgt_succ (* :(n:Z)`(Zs n) > n` *)
  97   Zorder.Zgt_pos_0 (* :(p:positive)`(POS p) > 0` *)
  98   Zplus_gt_compat_l (* :(n,m,p:Z)`n > m`->`p+n > p+m` *)
  99   Zplus_gt_compat_r (* :(n,m,p:Z)`n > m`->`n+p > m+p` *)
 100
 101   (* Lemmas ending by Zlt *)
 102   Zlt_succ (* :(n:Z)`n < (Zs n)` *)
 103   Zsucc_lt_compat (* :(n,m:Z)`n < m`->`(Zs n) < (Zs m)` *)
 104   Zlt_pred (* :(n:Z)`(Zpred n) < n` *)
 105   Zplus_lt_compat_l (* :(n,m,p:Z)`n < m`->`p+n < p+m` *)
 106   Zplus_lt_compat_r (* :(n,m,p:Z)`n < m`->`n+p < m+p` *)
 107
 108   (* Lemmas ending by Zle *)
 109   Zle_0_nat (* :(n:nat)`0 <= (inject_nat n)` *)
 110   Zorder.Zle_0_pos (* :(p:positive)`0 <= (POS p)` *)
 111   Zle_refl (* :(n:Z)`n <= n` *)
 112   Zle_succ (* :(n:Z)`n <= (Zs n)` *)
 113   Zsucc_le_compat (* :(n,m:Z)`m <= n`->`(Zs m) <= (Zs n)` *)
 114   Zle_pred (* :(n:Z)`(Zpred n) <= n` *)
 115   Zle_min_l (* :(n,m:Z)`(Zmin n m) <= n` *)
 116   Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *)
 117   Zplus_le_compat_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *)
 118   Zplus_le_compat_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *)
 119   Zabs_pos (* :(x:Z)`0 <= |x|` *)
 120
 121   (* B) Irreversible simplification lemmas : Probably to be declared as *)
 122   (* hints, when no other simplification is possible *)
 123
 124   (* Lemmas ending by eq *)
 125   BinInt.Z_eq_mult (* :(x,y:Z)`y = 0`->`y*x = 0` *)
 126   Zplus_eq_compat (* :(n,m,p,q:Z)`n = m`->`p = q`->`n+p = m+q` *)
 127
 128   (* Lemmas ending by Zge *)
 129   Zorder.Zmult_ge_compat_r (* :(a,b,c:Z)`a >= b`->`c >= 0`->`a*c >= b*c` *)
 130   Zorder.Zmult_ge_compat_l (* :(a,b,c:Z)`a >= b`->`c >= 0`->`c*a >= c*b` *)
 131   Zorder.Zmult_ge_compat (* :
 132       (a,b,c,d:Z)`a >= c`->`b >= d`->`c >= 0`->`d >= 0`->`a*b >= c*d` *)
 133
 134   (* Lemmas ending by Zlt *)
 135   Zorder.Zmult_gt_0_compat (* :(a,b:Z)`a > 0`->`b > 0`->`a*b > 0` *)
 136   Zlt_lt_succ (* :(n,m:Z)`n < m`->`n < (Zs m)` *)
 137
 138   (* Lemmas ending by Zle *)
 139   Zorder.Zmult_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x*y` *)
 140   Zorder.Zmult_le_compat_r (* :(a,b,c:Z)`a <= b`->`0 <= c`->`a*c <= b*c` *)
 141   Zorder.Zmult_le_compat_l (* :(a,b,c:Z)`a <= b`->`0 <= c`->`c*a <= c*b` *)
 142   Zplus_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x+y` *)
 143   Zle_le_succ (* :(x,y:Z)`x <= y`->`x <= (Zs y)` *)
 144   Zplus_le_compat (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *)
 145
 146   : zarith.
 147 *)
 148
 149 (*#*********************************************************************)
 150
 151 (*         Reversible lemmas relating operators                       *)
 152
 153 (* Probably to be declared as hints but need to define precedences    *)
 154
 155 (* A) Conversion between comparisons/predicates and arithmetic operators
 156
 157 (* Lemmas ending by eq *)
 158 Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0`
 159 Zabs_eq: (x:Z)`0 <= x`->`|x| = x`
 160 Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)`
 161 Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1`
 162
 163 (* Lemmas ending by Zgt *)
 164 Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y`
 165 Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0`
 166
 167 (* Lemmas ending by Zlt *)
 168 Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y`
 169 Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)`
 170 Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n`
 171
 172 (* Lemmas ending by Zle *)
 173 Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)`
 174 Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y`
 175 Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)`
 176 Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)`
 177 Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)`
 178
 179 (* B) Conversion between nat comparisons and Z comparisons *)
 180
 181 (* Lemmas ending by eq *)
 182 inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)`
 183
 184 (* Lemmas ending by Zge *)
 185 inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)`
 186
 187 (* Lemmas ending by Zgt *)
 188 inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)`
 189
 190 (* Lemmas ending by Zlt *)
 191 inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)`
 192
 193 (* Lemmas ending by Zle *)
 194 inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)`
 195
 196 (* C) Conversion between comparisons *)
 197
 198 (* Lemmas ending by Zge *)
 199 not_Zlt: (x,y:Z)~`x < y`->`x >= y`
 200 Zle_ge: (m,n:Z)`m <= n`->`n >= m`
 201
 202 (* Lemmas ending by Zgt *)
 203 Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n`
 204 not_Zle: (x,y:Z)~`x <= y`->`x > y`
 205 Zlt_gt: (m,n:Z)`m < n`->`n > m`
 206 Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n`
 207
 208 (* Lemmas ending by Zlt *)
 209 not_Zge: (x,y:Z)~`x >= y`->`x < y`
 210 Zgt_lt: (m,n:Z)`m > n`->`n < m`
 211 Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)`
 212
 213 (* Lemmas ending by Zle *)
 214 Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)`
 215 not_Zgt: (x,y:Z)~`x > y`->`x <= y`
 216 Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p`
 217 Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p`
 218 Zge_le: (m,n:Z)`m >= n`->`n <= m`
 219 Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p`
 220 Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m`
 221 Zlt_le_weak: (n,m:Z)`n < m`->`n <= m`
 222 Zle_refl: (n,m:Z)`n = m`->`n <= m`
 223
 224 (* D) Irreversible simplification involving several comparaisons, *)
 225 (*    useful with clear precedences *)
 226
 227 (* Lemmas ending by Zlt *)
 228 Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d`
 229 Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d`
 230
 231 (* D) What is decreasing here ? *)
 232
 233 (* Lemmas ending by eq *)
 234 Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m`
 235
 236 (* Lemmas ending by Zgt *)
 237 Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n`
 238
 239 (* Lemmas ending by Zlt *)
 240 Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)`
 241
 242 *)
 243
 244 (*#*********************************************************************)
 245
 246 (*                 Useful Bottom-up lemmas                            *)
 247
 248 (* A) Bottom-up simplification: should be used
 249
 250 (* Lemmas ending by eq *)
 251 Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m`
 252 Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p`
 253 Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m`
 254 Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m`
 255
 256 (* Lemmas ending by Zgt *)
 257 Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m`
 258 Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m`
 259 Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n`
 260
 261 (* Lemmas ending by Zlt *)
 262 Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m`
 263 Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m`
 264 Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m`
 265
 266 (* Lemmas ending by Zle *)
 267 Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m`
 268 Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m`
 269 Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n`
 270
 271 (* B) Bottom-up irreversible (syntactic) simplification *)
 272
 273 (* Lemmas ending by Zle *)
 274 Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m`
 275
 276 (* C) Other unclearly simplifying lemmas *)
 277
 278 (* Lemmas ending by Zeq *)
 279 Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0`
 280
 281 (* Lemmas ending by Zgt *)
 282 Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0`
 283
 284 (* Lemmas ending by Zlt *)
 285 pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y`
 286
 287 (* Lemmas ending by Zle *)
 288 Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y`
 289 OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y`
 290 *)
 291
 292 (*#*********************************************************************)
 293
 294 (*           Irreversible lemmas with meta-variables                  *)
 295
 296 (* To be used by EAuto
 297
 298 Hints Immediate
 299 (* Lemmas ending by eq *)
 300 Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m`
 301
 302 (* Lemmas ending by Zge *)
 303 Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p`
 304
 305 (* Lemmas ending by Zgt *)
 306 Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p`
 307 Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p`
 308 Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p`
 309 Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p`
 310
 311 (* Lemmas ending by Zlt *)
 312 Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p`
 313 Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p`
 314 Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p`
 315
 316 (* Lemmas ending by Zle *)
 317 Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p`
 318 *)
 319
 320 (*#*********************************************************************)
 321
 322 (*               Unclear or too specific lemmas                       *)
 323
 324 (* Not to be used ??                                                  *)
 325
 326 (* A) Irreversible and too specific (not enough regular)
 327
 328 (* Lemmas ending by Zle *)
 329 Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x`
 330 Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z`
 331 OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z`
 332 OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t`
 333
 334
 335 (* B) Expansion and too specific ? *)
 336
 337 (* Lemmas ending by Zge *)
 338 Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b`
 339
 340 (* Lemmas ending by Zgt *)
 341 Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b`
 342 Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y`
 343
 344 (* Lemmas ending by Zle *)
 345 Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b`
 346 Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y`
 347
 348 (* C) Reversible but too specific ? *)
 349
 350 (* Lemmas ending by Zlt *)
 351 Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
 352 *)
 353
 354 (*#*********************************************************************)
 355
 356 (*               Lemmas to be used as rewrite rules                   *)
 357
 358 (* but can also be used as hints
 359
 360 (* Left-to-right simplification lemmas (a symbol disappears) *)
 361
 362 Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m)
 363 Zmin_n_n: (n:Z)`(Zmin n n) = n`
 364 Zmult_1_n: (n:Z)`1*n = n`
 365 Zmult_n_1: (n:Z)`n*1 = n`
 366 Zminus_plus: (n,m:Z)`n+m-n = m`
 367 Zle_plus_minus: (n,m:Z)`n+(m-n) = m`
 368 Zopp_Zopp: (x:Z)`(-(-x)) = x`
 369 Zero_left: (x:Z)`0+x = x`
 370 Zero_right: (x:Z)`x+0 = x`
 371 Zplus_inverse_r: (x:Z)`x+(-x) = 0`
 372 Zplus_inverse_l: (x:Z)`(-x)+x = 0`
 373 Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y`
 374 Zmult_one: (x:Z)`1*x = x`
 375 Zero_mult_left: (x:Z)`0*x = 0`
 376 Zero_mult_right: (x:Z)`x*0 = 0`
 377 Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y`
 378
 379 (* Right-to-left simplification lemmas (a symbol disappears) *)
 380
 381 Zpred_Sn: (m:Z)`m = (Zpred (Zs m))`
 382 Zs_pred: (n:Z)`n = (Zs (Zpred n))`
 383 Zplus_n_O: (n:Z)`n = n+0`
 384 Zmult_n_O: (n:Z)`0 = n*0`
 385 Zminus_n_O: (n:Z)`n = n-0`
 386 Zminus_n_n: (n:Z)`0 = n-n`
 387 Zred_factor6: (x:Z)`x = x+0`
 388 Zred_factor0: (x:Z)`x = x*1`
 389
 390 (* Unclear orientation (no symbol disappears) *)
 391
 392 Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)`
 393 Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)`
 394 Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))`
 395 Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p`
 396 Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)`
 397 Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)`
 398 Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)`
 399 Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)`
 400 Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m`
 401 Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p`
 402 Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p`
 403 Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)`
 404 Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p`
 405 Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)`
 406 Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m`
 407 Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z`
 408 Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p`
 409 Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)`
 410 Zplus_sym: (x,y:Z)`x+y = y+x`
 411 Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z`
 412 Zmult_sym: (x,y:Z)`x*y = y*x`
 413 Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z`
 414 Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))`
 415 Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))`
 416 Zopp_one: (x:Z)`(-x) = x*(-1)`
 417 Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)`
 418 Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)`
 419 Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y`
 420 Zred_factor1: (x:Z)`x+x = x*2`
 421 Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)`
 422 Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)`
 423 Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)`
 424 Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y`
 425 Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n`
 426
 427 (* nat <-> Z *)
 428 inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))`
 429 inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)`
 430 inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)`
 431 inj_minus1:
 432  (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)`
 433 inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0`
 434
 435 (* Too specific ? *)
 436 Zred_factor5: (x,y:Z)`x*0+y = y`
 437 *)
 438
 439 (*i*)
 440