proposition: Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).
proof: Proof. intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). - solve_proper. - intros. now nzsimpl. - clear p Hp. intros p Hp IH n m. nzsimpl. assert (LR : forall n m, n < m -> p * n + n < p * m + m) by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). split; intros H. + now apply LR. + destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. * rewrite EQ in H. order. * apply LR in GT. order. Qed.
imports: NZAxioms NZAddOrder