On August 9, 2019 6:50:19 PM EDT, Norman Megill <n...@alum.mit.edu> wrote: >mvllmuld is essentially one direction of the more general divmuld. >Although we would need an extra mpbird to use divmuld instead, I think >mvllmuld is too specialized and would need a large number of uses to be >justified.
The purpose of algebra helpers like mvllmuld is not to make the proofs shorter, but to support a different style of proof. The idea is to enable moving an outermost expression from one side to the other of an equality statement using a single step. I think this approach sometimes results in easier to understand proofs, and it is closer to how I usually think about algebraic expressions (so I find the proofs easier to create). The whole point of the helpers is to make moving something from one side to the other a single step. So the fact that there are multistep approaches is true, but not relevant. I think it is worth doing, as the helpers can produce more human-friendly proofs (in my opinion). I do not know how many other people like them. It appears there is at least one other person, though! --- David A.Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/C2714687-B0DA-49DC-86F6-C74FFC710822%40dwheeler.com.
