Changeset 357 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Dec 1, 2010, 11:27:04 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r352 r357 4 4 include "Cartesian.ma". 5 5 include "Bool.ma". 6 7 6 include "Connectives.ma". 8 7 … … 655 654 #m n; napply less_than_b_elim. 656 655 nqed. 656 657 (* ===================================== *) 658 (* Numbers. *) 659 (* ===================================== *) 660 661 ndefinition one ≝ S Z. 662 ndefinition two ≝ (S(S(Z))). 663 ndefinition three ≝ two + one. 664 ndefinition four ≝ two + two. 665 ndefinition five ≝ three + two. 666 ndefinition six ≝ three + three. 667 ndefinition seven ≝ three + four. 668 ndefinition eight ≝ four + four. 669 ndefinition nine ≝ five + four. 670 ndefinition ten ≝ five + five. 671 ndefinition eleven ≝ six + five. 672 ndefinition twelve ≝ six + six. 673 ndefinition thirteen ≝ seven + six. 674 ndefinition fourteen ≝ seven + seven. 675 ndefinition fifteen ≝ eight + seven. 676 ndefinition sixteen ≝ eight + eight. 677 ndefinition seventeen ≝ nine + eight. 678 ndefinition eighteen ≝ nine + nine. 679 ndefinition nineteen ≝ ten + nine. 680 ndefinition twenty_four ≝ sixteen + eight. 681 ndefinition thirty_two ≝ sixteen + sixteen. 682 ndefinition one_hundred ≝ ten * ten. 683 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. 684 ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one. 685 ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one. 686 ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one. 687 ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven. 688 ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one. 689 ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one. 690 ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten. 691 ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one. 692 ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one. 693 ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one. 694 ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen. 695 ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight. 696 ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine. 697 ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen. 698 ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight. 699 ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen. 700 ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight. 701 ndefinition two_hundred ≝ one_hundred + one_hundred. 702 ndefinition two_hundred_and_two ≝ two_hundred + two. 703 ndefinition two_hundred_and_three ≝ two_hundred_and_two + one. 704 ndefinition two_hundred_and_four ≝ two_hundred_and_three + one. 705 ndefinition two_hundred_and_five ≝ two_hundred_and_four + one. 706 ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three. 707 ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen. 708 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen. 709 ndefinition two_hundred_and_fifty_six ≝ 710 one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.
Note: See TracChangeset
for help on using the changeset viewer.