Changeset 247 for Deliverables/D4.1/Matita/Nat.ma
- Timestamp:
- Nov 22, 2010, 11:12:56 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Nat.ma
r246 r247 311 311 //. 312 312 #N H. 313 //. 313 nnormalize. 314 nrewrite < H. 315 @. 314 316 nqed. 315 317 … … 355 357 #N H. 356 358 nnormalize. 357 //. 359 nrewrite > H. 360 nrewrite < (plus_associative n N ?). 361 nrewrite > (plus_symmetrical n N). 362 nrewrite > (plus_associative N n ?). 363 @. 358 364 nqed. 359 365 … … 374 380 nnormalize. 375 381 nrewrite > H. 376 napplyS multiplication_succ. 382 nrewrite > (multiplication_succ ? ?). 383 @. 377 384 nqed. 378 385 … … 386 393 #N H. 387 394 nnormalize. 388 //. 395 nrewrite > (succ_plus ? ?). 396 nrewrite < (succ_plus_succ_zero ?). 397 @. 389 398 nqed. 390 399 … … 412 421 nnormalize. 413 422 nrewrite > H. 414 napplyS plus_associative. 423 nrewrite < (plus_associative ? ? ?). 424 @. 415 425 nqed. 416 426 … … 419 429 o * (m + n) = o * m + o * n. 420 430 #m n o. 421 napplyS multiplication_symmetrical. 431 nelim o. 432 //. 433 #N H. 434 nnormalize. 435 nrewrite > H. 436 nrewrite < (plus_associative ? n (N * n)). 437 nrewrite > (plus_symmetrical (m + N * m) n). 438 nrewrite < (plus_associative n m (N * m)). 439 nrewrite < (plus_symmetrical n m). 440 nrewrite > (plus_associative (n + m) (N * m) (N * n)). 441 @. 422 442 nqed. 423 443 … … 432 452 nnormalize. 433 453 nrewrite > H. 434 napplyS multiplication_distributes_right_plus. 454 nrewrite > (multiplication_distributes_right_plus ? ? ?). 455 @. 435 456 nqed. 436 457
Note: See TracChangeset
for help on using the changeset viewer.