Theorem nat.one_succ_zero

fix(data): bitvec and vector are in the main repo

refactor(*): use 'lemma' iff statement is private

refactor(*): import content from lean/library/data and library_dev