Theorem linear_order_cases_on_eq

feat(data/num,data/nat/cast,...): nat,num,int,rat.cast, list stuff

feat(data/rat): new rat representation using canonical elements …

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

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