Library Stdlib.Numbers.NatInt.NZMulOrder

Properties of orders and multiplication for modules implementing NZOrdAxiomsSig'

This file defines the NZMulOrderProp functor type, meant to be Included in a module implementing NZOrdAxiomsSig' (see Stdlib.Numbers.NatInt.NZAxioms).

This gives important basic compatibility lemmas between mul and lt, le. It also gives cancellation lemmas between mul and eq.

Since it applies both to natural numbers and integers, some of these lemmas have nonnegativity conditions which could disappear when used with natural numbers.

Notice that NZMulOrderProp Includes NZAddOrderProp.

From Stdlib Require Import NZAxioms.
From Stdlib Require Import NZAddOrder.

Module Type NZMulOrderProp (Import NZ : NZOrdAxiomsSig').
Include NZAddOrderProp NZ.

Theorem mul_lt_pred :
  forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n ).

Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m ).

Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p ).

Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n ).

Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p ).

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

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

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

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

Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m ).

Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m ).

Lemma mul_reg_l n m p : p ~= 0 -> p * n == p * m -> n == m.

Lemma mul_reg_r n m p : p ~= 0 -> n * p == m * p -> n == m.

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

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

Theorem mul_le_mono_pos_l : forall n m p, 0 < p -> (n <= m <-> p * n <= p * m ).

Theorem mul_le_mono_pos_r : forall n m p, 0 < p -> (n <= m <-> n * p <= m * p ).

Theorem mul_le_mono_neg_l : forall n m p, p < 0 -> (n <= m <-> p * m <= p * n ).

Theorem mul_le_mono_neg_r : forall n m p, p < 0 -> (n <= m <-> m * p <= n * p ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0.

Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0.

Notation mul_eq_0 := eq_mul_0.
Notation mul_eq_0_l := eq_mul_0_l.
Notation mul_eq_0_r := eq_mul_0_r.

Theorem lt_0_mul n m : 0 < n * m <-> (0 < n /\ 0 < m ) \/ (m < 0 /\ n < 0).

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

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

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

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

Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m.

Lemma add_le_mul : forall a b, 1<a -> 1<b -> a +b <= a *b.

A few results about squares

Lemma square_nonneg : forall a, 0 <= a * a.

Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b *a +a *b <= a *a +b *b.

Lemma add_square_le : forall a b, 0<=a -> 0<=b ->
a *a + b *b <= (a +b )*(a +b ).

Lemma square_add_le : forall a b, 0<=a -> 0<=b ->
(a +b )*(a +b ) <= 2*(a *a + b *b ).

Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b ->
2*2*a *b <= (a +b )*(a +b ).

End NZMulOrderProp.