Library Coq.Numbers.Integer.Abstract.ZMulOrder



Require Export ZAddOrder.

Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig').
Include ZAddOrderPropFunct Z.

Local Notation "- 1" := (-(1)).

Theorem mul_lt_mono_nonpos :
  forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p.

Theorem mul_le_mono_nonpos :
  forall n m p q, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p.

Theorem mul_nonpos_nonpos : forall n m, n <= 0 -> m <= 0 -> 0 <= n * m.

Theorem mul_nonneg_nonpos : forall n m, 0 <= n -> m <= 0 -> n * m <= 0.

Theorem mul_nonpos_nonneg : forall n m, n <= 0 -> 0 <= m -> n * m <= 0.

Notation mul_pos := lt_0_mul (only parsing).

Theorem lt_mul_0 :
  forall n m, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0.

Notation mul_neg := lt_mul_0 (only parsing).

Theorem le_0_mul :
  forall n m, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.

Notation mul_nonneg := le_0_mul (only parsing).

Theorem le_mul_0 :
  forall n m, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.

Notation mul_nonpos := le_mul_0 (only parsing).

Theorem le_0_square : forall n, 0 <= n * n.

Notation square_nonneg := le_0_square (only parsing).

Theorem nlt_square_0 : forall n, ~ n * n < 0.

Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m.

Theorem square_le_mono_nonpos : forall n m, n <= 0 -> m <= n -> n * n <= m * m.

Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n.

Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n.

Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m.

Theorem lt_mul_n1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1.

Theorem lt_mul_n1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1.

Theorem lt_1_mul_l : forall n m, 1 < n ->
 n * m < -1 \/ n * m == 0 \/ 1 < n * m.

Theorem lt_n1_mul_r : forall n m, n < -1 ->
 n * m < -1 \/ n * m == 0 \/ 1 < n * m.

Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.

Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n).

Theorem lt_mul_diag_r : forall n m, 0 < n -> (1 < m <-> n < n * m).

Theorem le_mul_diag_l : forall n m, n < 0 -> (1 <= m <-> n * m <= n).

Theorem le_mul_diag_r : forall n m, 0 < n -> (1 <= m <-> n <= n * m).

Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p.

End ZMulOrderPropFunct.