feat(library/standard/int): prove more theorems about le, define mul

Prove most interactions of le with other operators. Define multiplication, and prove that it is compatible with the relation on N ## N