qed.
theorem lt_to_le_to_lt_times:
∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
#n #m #p #q #ltnm #lepq #posq
@(le_to_lt_to_lt ? (n*q))
qed.
theorem lt_to_le_to_lt_times:
∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
#n #m #p #q #ltnm #lepq #posq
@(le_to_lt_to_lt ? (n*q))