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 :