Commit 2022-03-03 21:31 54c286db

feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about star on casts (#12418) This also includes lemmas about mul_opposite on casts which are used to prove the star lemmas. The new lemmas are:

• star_nat_cast
• star_int_cast
• star_rat_cast
• op_nat_cast
• op_int_cast
• op_rat_cast
• unop_nat_cast
• unop_int_cast
• unop_rat_cast