Changeset 1587 for src/utilities/binary
 Timestamp:
 Dec 5, 2011, 5:16:55 PM (10 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.