proposition: Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
proof: Proof. intros p q n m H. rewrite <- H. nzsimpl. rewrite <- ! add_assoc, (add_comm n m). now rewrite <- add_lt_mono_r. Qed.
imports: NZAxioms NZAddOrder