Theorem nat.succ_add_eq_succ_add

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

refactor(*): attributes on same line

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