Ignore:
Timestamp:
Nov 10, 2010, 5:26:08 PM (10 years ago)
Author:
mulligan
Message:

Lots of work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Nat.ma

    r228 r230  
    108108nqed.
    109109
    110 nlemma multiplication_zero:
     110nlemma multiplication_zero_right_neutral:
    111111  ∀m: Nat.
    112112    m * Z = Z.
     
    151151  napplyS multiplication_succ.
    152152nqed.
    153  
     153
     154nlemma multiplication_succ_zero_left_neutral:
     155  ∀m: Nat.
     156    (S Z) * m = m.
     157  #m.
     158  nelim m.
     159  nnormalize.
     160  @.
     161  #N H.
     162  nnormalize.
     163  napplyS succ_plus.
     164nqed.
     165
     166nlemma multiplication_succ_zero_right_neutral:
     167  ∀m: Nat.
     168    m * (S Z) = m.
     169  #m.
     170  nelim m.
     171  nnormalize.
     172  @.
     173  #N H.
     174  nnormalize.
     175  nrewrite > H.
     176  @.
     177nqed.
     178
     179nlemma multiplication_distributes_right_plus:
     180  ∀m, n, o: Nat.
     181    (m + n) * o = m * o + n * o.
     182  #m n o.
     183  nelim m.
     184  nnormalize.
     185  @.
     186  #N H.
     187  nnormalize.
     188  nrewrite > H.
     189  napplyS plus_associative.
     190nqed.
     191
     192nlemma multiplication_distributes_left_plus:
     193  ∀m, n, o: Nat.
     194    o * (m + n) = o * m + o * n.
     195  #m n o.
     196  napplyS multiplication_symmetrical.
     197nqed.
     198
     199nlemma mutliplication_associative:
     200  ∀m, n, o: Nat.
     201    m * (n * o) = (m * n) * o.
     202  #m n o.
     203  nelim m.
     204  nnormalize.
     205  @.
     206  #N H.
     207  nnormalize.
     208  nrewrite > H.
     209  napplyS multiplication_distributes_right_plus.
     210nqed.
     211
     212nlemma minus_minus:
     213  ∀n: Nat.
     214    n - n = Z.
     215  #n.
     216  nelim n.
     217  nnormalize.
     218  @.
     219  #N H.
     220  nnormalize.
     221  nrewrite > H.
     222  @.
     223nqed.
     224
     225(*
     226nlemma succ_injective:
     227  ∀m, n: Nat.
     228    S m = S n → m = n.
     229  #m n.
     230  nelim m.
     231  #H.
     232  ninversion H.
     233  #H.
     234  ndestruct
     235
     236nlemma plus_minus_associate:
     237  ∀m, n, o: Nat.
     238    (m + n) - o = m + (n - o).
     239  #m n o.
     240  nelim m.
     241  nnormalize.
     242  @.
     243  #N H.
     244 
     245
     246nlemma plus_minus_inverses:
     247  ∀m, n: Nat.
     248    (m + n) - n = m.
     249  #m n.
     250  nelim m.
     251  nnormalize.
     252  napply minus_minus.
     253  #N H.
     254*)
Note: See TracChangeset for help on using the changeset viewer.