ZMulOrder.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

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.forall n m p q : t,
m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p
Proof.forall n m p q : t,
m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p
intros n m p q H1 H2 H3 H4.n, m, p, q:t
H1:m <= 0
H2:n < m
H3:q <= 0
H4:p < q
m * q < n * p
apply le_lt_trans with (m * p).n, m, p, q:t
H1:m <= 0
H2:n < m
H3:q <= 0
H4:p < q
m * q <= m * p
n, m, p, q:t
H1:m <= 0
H2:n < m
H3:q <= 0
H4:p < q
m * p < n * p
apply mul_le_mono_nonpos_l; [assumption | now apply lt_le_incl].n, m, p, q:t
H1:m <= 0
H2:n < m
H3:q <= 0
H4:p < q
m * p < n * p
apply -> mul_lt_mono_neg_r; [assumption | now apply lt_le_trans with q].
Qed.

Theorem mul_le_mono_nonpos :
  forall n m p q, m <= 0 -> n <= m -> q <= 0 -> p <= q ->  m * q <= n * p.forall n m p q : t,
m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p
Proof.forall n m p q : t,
m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p
intros n m p q H1 H2 H3 H4.n, m, p, q:t
H1:m <= 0
H2:n <= m
H3:q <= 0
H4:p <= q
m * q <= n * p
apply le_trans with (m * p).n, m, p, q:t
H1:m <= 0
H2:n <= m
H3:q <= 0
H4:p <= q
m * q <= m * p
n, m, p, q:t
H1:m <= 0
H2:n <= m
H3:q <= 0
H4:p <= q
m * p <= n * p
now apply mul_le_mono_nonpos_l.n, m, p, q:t
H1:m <= 0
H2:n <= m
H3:q <= 0
H4:p <= q
m * p <= n * p
apply mul_le_mono_nonpos_r; [now apply le_trans with q | assumption].
Qed.

Theorem mul_nonpos_nonpos : forall n m, n <= 0 -> m <= 0 -> 0 <= n * m.forall n m : t, n <= 0 -> m <= 0 -> 0 <= n * m
Proof.forall n m : t, n <= 0 -> m <= 0 -> 0 <= n * m
intros n m H1 H2.n, m:t
H1:n <= 0
H2:m <= 0
0 <= n * m
rewrite <- (mul_0_l m).n, m:t
H1:n <= 0
H2:m <= 0
0 * m <= n * m now apply mul_le_mono_nonpos_r.
Qed.

Theorem mul_nonneg_nonpos : forall n m, 0 <= n -> m <= 0 -> n * m <= 0.forall n m : t, 0 <= n -> m <= 0 -> n * m <= 0
Proof.forall n m : t, 0 <= n -> m <= 0 -> n * m <= 0
intros n m H1 H2.n, m:t
H1:0 <= n
H2:m <= 0
n * m <= 0
rewrite <- (mul_0_l m).n, m:t
H1:0 <= n
H2:m <= 0
n * m <= 0 * m now apply mul_le_mono_nonpos_r.
Qed.

Theorem mul_nonpos_nonneg : forall n m, n <= 0 -> 0 <= m -> n * m <= 0.forall n m : t, n <= 0 -> 0 <= m -> n * m <= 0
Proof.forall n m : t, n <= 0 -> 0 <= m -> n * m <= 0
intros; rewrite mul_comm; now apply mul_nonneg_nonpos.
Qed.

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.forall n m : t,
n * m < 0 <-> n < 0 < m \/ 0 < n /\ m < 0
Proof.forall n m : t,
n * m < 0 <-> n < 0 < m \/ 0 < n /\ m < 0
intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].n, m:t
H:n * m < 0
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |];
(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]);
try (left; now split); try (right; now split).n, m:t
H:n * m < 0
H1:n < 0
H2:m < 0
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H:n * m < 0
H1:0 < n
H2:0 < m
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
assert (H3 : n * m > 0) by now apply mul_neg_neg.n, m:t
H:n * m < 0
H1:n < 0
H2:m < 0
H3:0 < n * m
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H:n * m < 0
H1:0 < n
H2:0 < m
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
exfalso; now apply (lt_asymm (n * m) 0).n, m:t
H:n * m < 0
H1:0 < n
H2:0 < m
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
assert (H3 : n * m > 0) by now apply mul_pos_pos.n, m:t
H:n * m < 0
H1:0 < n
H2:0 < m
H3:0 < n * m
n < 0 < m \/ 0 < n /\ m < 0
n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
exfalso; now apply (lt_asymm (n * m) 0).n, m:t
H1:n < 0
H2:0 < m
n * m < 0
n, m:t
H1:0 < n
H2:m < 0
n * m < 0
now apply mul_neg_pos.n, m:t
H1:0 < n
H2:m < 0
n * m < 0 now apply mul_pos_neg.
Qed.

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.forall n m : t,
0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0
Proof.forall n m : t,
0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0
assert (R : forall n, 0 == n <-> n == 0) by (intros; split; apply eq_sym).R:forall n : t, 0 == n <-> n == 0
forall n m : t,
0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0
intros n m.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0 repeat rewrite lt_eq_cases.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
0 < n * m \/ 0 == n * m ->
(0 < n \/ 0 == n) /\ (0 < m \/ 0 == m) \/
(n < 0 \/ n == 0) /\ (m < 0 \/ m == 0) repeat rewrite R.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
0 < n * m \/ n * m == 0 ->
(0 < n \/ n == 0) /\ (0 < m \/ m == 0) \/
(n < 0 \/ n == 0) /\ (m < 0 \/ m == 0)
rewrite lt_0_mul, eq_mul_0.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
(0 < n /\ 0 < m \/ m < 0 /\ n < 0) \/ n == 0 \/ m == 0 ->
(0 < n \/ n == 0) /\ (0 < m \/ m == 0) \/
(n < 0 \/ n == 0) /\ (m < 0 \/ m == 0)
pose proof (lt_trichotomy n 0); pose proof (lt_trichotomy m 0).R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
H:n < 0 \/ n == 0 \/ 0 < n
H0:m < 0 \/ m == 0 \/ 0 < m
(0 < n /\ 0 < m \/ m < 0 /\ n < 0) \/ n == 0 \/ m == 0 ->
(0 < n \/ n == 0) /\ (0 < m \/ m == 0) \/
(n < 0 \/ n == 0) /\ (m < 0 \/ m == 0) tauto.
Qed.

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.forall n m : t,
n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 <= m
Proof.forall n m : t,
n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 <= m
assert (R : forall n, 0 == n <-> n == 0) by (intros; split; apply eq_sym).R:forall n : t, 0 == n <-> n == 0
forall n m : t,
n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 <= m
intros n m.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 <= m repeat rewrite lt_eq_cases.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
n * m < 0 \/ n * m == 0 ->
(0 < n \/ 0 == n) /\ (m < 0 \/ m == 0) \/
(n < 0 \/ n == 0) /\ (0 < m \/ 0 == m) repeat rewrite R.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
n * m < 0 \/ n * m == 0 ->
(0 < n \/ n == 0) /\ (m < 0 \/ m == 0) \/
(n < 0 \/ n == 0) /\ (0 < m \/ m == 0)
rewrite lt_mul_0, eq_mul_0.R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
(n < 0 < m \/ 0 < n /\ m < 0) \/ n == 0 \/ m == 0 ->
(0 < n \/ n == 0) /\ (m < 0 \/ m == 0) \/
(n < 0 \/ n == 0) /\ (0 < m \/ m == 0)
pose proof (lt_trichotomy n 0); pose proof (lt_trichotomy m 0).R:forall n0 : t, 0 == n0 <-> n0 == 0
n, m:t
H:n < 0 \/ n == 0 \/ 0 < n
H0:m < 0 \/ m == 0 \/ 0 < m
(n < 0 < m \/ 0 < n /\ m < 0) \/ n == 0 \/ m == 0 ->
(0 < n \/ n == 0) /\ (m < 0 \/ m == 0) \/
(n < 0 \/ n == 0) /\ (0 < m \/ m == 0) tauto.
Qed.

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.forall n : t, ~ n * n < 0
Proof.forall n : t, ~ n * n < 0
intros n H.n:t
H:n * n < 0
False apply lt_nge in H.n:t
H:~ 0 <= n * n
False apply H.n:t
H:~ 0 <= n * n
0 <= n * n apply square_nonneg.
Qed.

Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m.forall n m : t, n <= 0 -> m < n -> n * n < m * m
Proof.forall n m : t, n <= 0 -> m < n -> n * n < m * m
intros n m H1 H2.n, m:t
H1:n <= 0
H2:m < n
n * n < m * m now apply mul_lt_mono_nonpos.
Qed.

Theorem square_le_mono_nonpos : forall n m, n <= 0 -> m <= n -> n * n <= m * m.forall n m : t, n <= 0 -> m <= n -> n * n <= m * m
Proof.forall n m : t, n <= 0 -> m <= n -> n * n <= m * m
intros n m H1 H2.n, m:t
H1:n <= 0
H2:m <= n
n * n <= m * m now apply mul_le_mono_nonpos.
Qed.

Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n.forall n m : t, m <= 0 -> n * n < m * m -> m < n
Proof.forall n m : t, m <= 0 -> n * n < m * m -> m < n
intros n m H1 H2.n, m:t
H1:m <= 0
H2:n * n < m * m
m < n destruct (le_gt_cases n 0); [|order].n, m:t
H1:m <= 0
H2:n * n < m * m
H:n <= 0
m < n
destruct (lt_ge_cases m n) as [LE|GT]; trivial.n, m:t
H1:m <= 0
H2:n * n < m * m
H:n <= 0
GT:n <= m
m < n
apply square_le_mono_nonpos in GT; order.
Qed.

Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n.forall n m : t, m <= 0 -> n * n <= m * m -> m <= n
Proof.forall n m : t, m <= 0 -> n * n <= m * m -> m <= n
intros n m H1 H2.n, m:t
H1:m <= 0
H2:n * n <= m * m
m <= n destruct (le_gt_cases n 0); [|order].n, m:t
H1:m <= 0
H2:n * n <= m * m
H:n <= 0
m <= n
destruct (le_gt_cases m n) as [LE|GT]; trivial.n, m:t
H1:m <= 0
H2:n * n <= m * m
H:n <= 0
GT:n < m
m <= n
apply square_lt_mono_nonpos in GT; order.
Qed.

Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m.forall n m : t, n < -1 -> m < 0 -> 1 < n * m
Proof.forall n m : t, n < -1 -> m < 0 -> 1 < n * m
intros n m H1 H2.n, m:t
H1:n < -1
H2:m < 0
1 < n * m apply (mul_lt_mono_neg_r m) in H1.n, m:t
H1:-1 * m < n * m
H2:m < 0
1 < n * m
n, m:t
H1:n < -1
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0
apply opp_pos_neg in H2.n, m:t
H1:-1 * m < n * m
H2:0 < - m
1 < n * m
n, m:t
H1:n < -1
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0 rewrite mul_opp_l, mul_1_l in H1.n, m:t
H1:- m < n * m
H2:0 < - m
1 < n * m
n, m:t
H1:n < -1
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0
now apply lt_1_l with (- m).n, m:t
H1:n < -1
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0
assumption.
Qed.

Theorem lt_mul_m1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1.forall n m : t, 1 < n -> m < 0 -> n * m < -1
Proof.forall n m : t, 1 < n -> m < 0 -> n * m < -1
intros n m H1 H2.n, m:t
H1:1 < n
H2:m < 0
n * m < -1 apply (mul_lt_mono_neg_r m) in H1.n, m:t
H1:n * m < 1 * m
H2:m < 0
n * m < -1
n, m:t
H1:1 < n
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0
rewrite mul_1_l in H1.n, m:t
H1:n * m < m
H2:m < 0
n * m < -1
n, m:t
H1:1 < n
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0 now apply lt_m1_r with m.n, m:t
H1:1 < n
H2:m < 0
H:forall n0 m0 : t,
m < 0 -> n0 < m0 -> m0 * m < n0 * m
m < 0
assumption.
Qed.

Theorem lt_mul_m1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1.forall n m : t, n < -1 -> 0 < m -> n * m < -1
Proof.forall n m : t, n < -1 -> 0 < m -> n * m < -1
intros n m H1 H2.n, m:t
H1:n < -1
H2:0 < m
n * m < -1 apply (mul_lt_mono_pos_r m) in H1.n, m:t
H1:n * m < -1 * m
H2:0 < m
n * m < -1
n, m:t
H1:n < -1
H2:0 < m
H:forall n0 m0 : t,
0 < m -> n0 < m0 -> n0 * m < m0 * m
0 < m
rewrite mul_opp_l, mul_1_l in H1.n, m:t
H1:n * m < - m
H2:0 < m
n * m < -1
n, m:t
H1:n < -1
H2:0 < m
H:forall n0 m0 : t,
0 < m -> n0 < m0 -> n0 * m < m0 * m
0 < m
apply opp_neg_pos in H2.n, m:t
H1:n * m < - m
H2:- m < 0
n * m < -1
n, m:t
H1:n < -1
H2:0 < m
H:forall n0 m0 : t,
0 < m -> n0 < m0 -> n0 * m < m0 * m
0 < m now apply lt_m1_r with (- m).n, m:t
H1:n < -1
H2:0 < m
H:forall n0 m0 : t,
0 < m -> n0 < m0 -> n0 * m < m0 * m
0 < m
assumption.
Qed.

Theorem lt_1_mul_l : forall n m, 1 < n ->
 n * m < -1 \/ n * m == 0 \/ 1 < n * m.forall n m : t,
1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m
Proof.forall n m : t,
1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m
intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]].n, m:t
H:1 < n
H1:m < 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:1 < n
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:1 < n
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
left.n, m:t
H:1 < n
H1:m < 0
n * m < -1
n, m:t
H:1 < n
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:1 < n
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m now apply lt_mul_m1_neg.n, m:t
H:1 < n
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:1 < n
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
right; left; now rewrite H1, mul_0_r.n, m:t
H:1 < n
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
right; right; now apply lt_1_mul_pos.
Qed.

Theorem lt_m1_mul_r : forall n m, n < -1 ->
 n * m < -1 \/ n * m == 0 \/ 1 < n * m.forall n m : t,
n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m
Proof.forall n m : t,
n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m
intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]].n, m:t
H:n < -1
H1:m < 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:n < -1
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:n < -1
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
right; right.n, m:t
H:n < -1
H1:m < 0
1 < n * m
n, m:t
H:n < -1
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:n < -1
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m now apply lt_1_mul_neg.n, m:t
H:n < -1
H1:m == 0
n * m < -1 \/ n * m == 0 \/ 1 < n * m
n, m:t
H:n < -1
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
right; left; now rewrite H1, mul_0_r.n, m:t
H:n < -1
H1:0 < m
n * m < -1 \/ n * m == 0 \/ 1 < n * m
left.n, m:t
H:n < -1
H1:0 < m
n * m < -1 now apply lt_mul_m1_pos.
Qed.

Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.forall n m : t, n * m == 1 -> n == 1 \/ n == -1
Proof.forall n m : t, n * m == 1 -> n == 1 \/ n == -1
assert (F := lt_m1_0).F:-1 < 0
forall n m : t, n * m == 1 -> n == 1 \/ n == -1
zero_pos_neg n.F:-1 < 0
forall m : t, 0 * m == 1 -> 0 == 1 \/ 0 == -1
F:-1 < 0
forall n : t,
0 < n ->
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1)
(* n = 0 *)
intros m.F:-1 < 0
m:t
0 * m == 1 -> 0 == 1 \/ 0 == -1
F:-1 < 0
forall n : t,
0 < n ->
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1) nzsimpl.F:-1 < 0
m:t
0 == 1 -> 0 == 1 \/ 0 == -1
F:-1 < 0
forall n : t,
0 < n ->
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1) now left.F:-1 < 0
forall n : t,
0 < n ->
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1)
(* 0 < n, proving P n /\ P (-n) *)
intros n Hn.F:-1 < 0
n:t
Hn:0 < n
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1) rewrite <- le_succ_l, <- one_succ in Hn.F:-1 < 0
n:t
Hn:1 <= n
(forall m : t, n * m == 1 -> n == 1 \/ n == -1) /\
(forall m : t, - n * m == 1 -> - n == 1 \/ - n == -1)
le_elim Hn; split; intros m H.F:-1 < 0
n:t
Hn:1 < n
m:t
H:n * m == 1
n == 1 \/ n == -1
F:-1 < 0
n:t
Hn:1 < n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:n * m == 1
n == 1 \/ n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
destruct (lt_1_mul_l n m) as [|[|]]; order'.F:-1 < 0
n:t
Hn:1 < n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:n * m == 1
n == 1 \/ n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
rewrite mul_opp_l, eq_opp_l in H.F:-1 < 0
n:t
Hn:1 < n
m:t
H:n * m == -1
- n == 1 \/ - n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:n * m == 1
n == 1 \/ n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1 destruct (lt_1_mul_l n m) as [|[|]]; order'.F:-1 < 0
n:t
Hn:1 == n
m:t
H:n * m == 1
n == 1 \/ n == -1
F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
now left.F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == 1 \/ - n == -1
intros; right.F:-1 < 0
n:t
Hn:1 == n
m:t
H:- n * m == 1
- n == -1 now f_equiv.
Qed.

Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n).forall n m : t, n < 0 -> 1 < m <-> n * m < n
Proof.forall n m : t, n < 0 -> 1 < m <-> n * m < n
intros n m H.n, m:t
H:n < 0
1 < m <-> n * m < n stepr (n * m < n * 1) by now rewrite mul_1_r.n, m:t
H:n < 0
1 < m <-> n * m < n * 1
now apply mul_lt_mono_neg_l.
Qed.

Theorem lt_mul_diag_r : forall n m, 0 < n -> (1 < m <-> n < n * m).forall n m : t, 0 < n -> 1 < m <-> n < n * m
Proof.forall n m : t, 0 < n -> 1 < m <-> n < n * m
intros n m H.n, m:t
H:0 < n
1 < m <-> n < n * m stepr (n * 1 < n * m) by now rewrite mul_1_r.n, m:t
H:0 < n
1 < m <-> n * 1 < n * m
now apply mul_lt_mono_pos_l.
Qed.

Theorem le_mul_diag_l : forall n m, n < 0 -> (1 <= m <-> n * m <= n).forall n m : t, n < 0 -> 1 <= m <-> n * m <= n
Proof.forall n m : t, n < 0 -> 1 <= m <-> n * m <= n
intros n m H.n, m:t
H:n < 0
1 <= m <-> n * m <= n stepr (n * m <= n * 1) by now rewrite mul_1_r.n, m:t
H:n < 0
1 <= m <-> n * m <= n * 1
now apply mul_le_mono_neg_l.
Qed.

Theorem le_mul_diag_r : forall n m, 0 < n -> (1 <= m <-> n <= n * m).forall n m : t, 0 < n -> 1 <= m <-> n <= n * m
Proof.forall n m : t, 0 < n -> 1 <= m <-> n <= n * m
intros n m H.n, m:t
H:0 < n
1 <= m <-> n <= n * m stepr (n * 1 <= n * m) by now rewrite mul_1_r.n, m:t
H:0 < n
1 <= m <-> n * 1 <= n * m
now apply mul_le_mono_pos_l.
Qed.

Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p.forall n m p : t, 0 < n -> 1 < p -> n < m -> n < m * p
Proof.forall n m p : t, 0 < n -> 1 < p -> n < m -> n < m * p
intros.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
n < m * p stepl (n * 1) by now rewrite mul_1_r.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
n * 1 < m * p
apply mul_lt_mono_nonneg.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
0 <= n
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
n < m
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
0 <= 1
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
1 < p
now apply lt_le_incl.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
n < m
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
0 <= 1
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
1 < p assumption.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
0 <= 1
n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
1 < p apply le_0_1.n, m, p:t
H:0 < n
H0:1 < p
H1:n < m
1 < p assumption.
Qed.

Alternative name :

Definition mul_eq_1 := eq_mul_1.

End ZMulOrderProp.