proposition: Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
proof: Proof. intro p; nzord_induct p. - order. - intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. - intros p Hp IH n m _. apply le_succ_l in Hp. le_elim Hp. + assert (LR : forall n m, n < m -> p * m < p * n). * intros n1 m1 H. apply (le_lt_add_lt n1 m1). -- now apply lt_le_incl. -- rewrite <- 2 mul_succ_l. 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. + rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. Qed.
imports: NZAxioms NZAddOrder