linear_ordered_semiring theorems

Stream: maths

[Mario Carneiro]

zero_lt_two, one_lt_two, lt_add_one, lt_one_add, bit1_pos, one_lt_mul, mul_le_one, one_lt_mul_of_le_of_lt, and several others all assume linear_ordered_semiring, while the linear order does not appear necessary here since there is no multiplicative cancellation going on

[Mario Carneiro]

(While I'm at it, now's the time to suggest weaker typeclass assumptions on the core norm_num theorems. I know that there was a problem with working with division in complex because it makes unjustified linear order assumptions, and I haven't addressed that yet.)