feat(library/standard): finish everything(?) about mul, le, lt, add sign

Prove everything about multiplication, inequalities, and interactions. Add sign function, and prove some properties about it.