Commit 2020-07-09 15:24 593a4c83

fix(tactic/norm_cast): remove bad norm_cast lemma (#3340) This was identified as a move_cast lemma, which meant it was rewriting to the LHS which it couldn't reduce. It's better to let the conditional rewriting handle nat subtraction -- if the right inequality is in the context there's no need to go to int.sub_nat_nat.