Changeset 1587 for src/utilities/binary
- Timestamp:
- Dec 5, 2011, 5:16:55 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/binary/positive.ma
r1528 r1587 852 852 853 853 theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. 854 #n elim n; //; qed .854 #n elim n; //; qed-. 855 855 856 856 theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
Note: See TracChangeset
for help on using the changeset viewer.