Library Coq.Numbers.Integer.Abstract.ZMulOrder


Require Export ZAddOrder.

Module Type ZMulOrderProp (Import Z : ZAxiomsMiniSig').
Include ZAddOrderProp Z.

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).

Notation le_0_square := square_nonneg (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_m1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1.

Theorem lt_mul_m1_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_m1_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.

Alternative name :

Definition mul_eq_1 := eq_mul_1.

End ZMulOrderProp.