NZMulOrder.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 Import NZAxioms.
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).forall p q n m : t,
S p == q -> p * n < p * m <-> q * n + m < q * m + n
Proof.forall p q n m : t,
S p == q -> p * n < p * m <-> q * n + m < q * m + n
intros p q n m H.p, q, n, m:t
H:S p == q
p * n < p * m <-> q * n + m < q * m + n rewrite <- H.p, q, n, m:t
H:S p == q
p * n < p * m <-> S p * n + m < S p * m + n nzsimpl.p, q, n, m:t
H:S p == q
p * n < p * m <-> p * n + n + m < p * m + m + n
rewrite <- ! add_assoc, (add_comm n m).p, q, n, m:t
H:S p == q
p * n < p * m <-> p * n + (m + n) < p * m + (m + n)
now rewrite <- add_lt_mono_r.
Qed.

Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).forall p n m : t, 0 < p -> n < m <-> p * n < p * m
Proof.forall p n m : t, 0 < p -> n < m <-> p * n < p * m
  intros p n m Hp.p, n, m:t
Hp:0 < p
n < m <-> p * n < p * m revert n m.p:t
Hp:0 < p
forall n m : t, n < m <-> p * n < p * m apply lt_ind with (4:=Hp).p:t
Hp:0 < p
Proper (eq ==> iff)
  (fun p0 : t =>
   forall n m : t, n < m <-> p0 * n < p0 * m)
p:t
Hp:0 < p
forall n m : t, n < m <-> S 0 * n < S 0 * m
p:t
Hp:0 < p
forall m : t,
0 < m ->
(forall n m0 : t, n < m0 <-> m * n < m * m0) ->
forall n m0 : t, n < m0 <-> S m * n < S m * m0 -p:t
Hp:0 < p
Proper (eq ==> iff)
  (fun p0 : t =>
   forall n m : t, n < m <-> p0 * n < p0 * m) solve_proper.
  -p:t
Hp:0 < p
forall n m : t, n < m <-> S 0 * n < S 0 * m intros.p:t
Hp:0 < p
n, m:t
n < m <-> S 0 * n < S 0 * m now nzsimpl.
  -p:t
Hp:0 < p
forall m : t,
0 < m ->
(forall n m0 : t, n < m0 <-> m * n < m * m0) ->
forall n m0 : t, n < m0 <-> S m * n < S m * m0 clear p Hp.forall m : t,
0 < m ->
(forall n m0 : t, n < m0 <-> m * n < m * m0) ->
forall n m0 : t, n < m0 <-> S m * n < S m * m0 intros p Hp IH n m.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
n < m <-> S p * n < S p * m nzsimpl.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
n < m <-> p * n + n < p * m + m
    assert (LR : forall n m, n < m -> p * n + n < p * m + m)
      by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH).p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
n < m <-> p * n + n < p * m + m
    split; intros H.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:n < m
p * n + n < p * m + m
p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
n < m
    +p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:n < m
p * n + n < p * m + m now apply LR.
    +p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
n < m destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
EQ:n == m
n < m
p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
GT:m < n
n < m
      *p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
EQ:n == m
n < m rewrite EQ in H.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * m + m < p * m + m
EQ:n == m
n < m order.
      *p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
GT:m < n
n < m apply LR in GT.p:t
Hp:0 < p
IH:forall n0 m0 : t, n0 < m0 <-> p * n0 < p * m0
n, m:t
LR:forall n0 m0 : t,
n0 < m0 -> p * n0 + n0 < p * m0 + m0
H:p * n + n < p * m + m
GT:p * m + m < p * n + n
n < m order.
Qed.

Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p).forall p n m : t, 0 < p -> n < m <-> n * p < m * p
Proof.forall p n m : t, 0 < p -> n < m <-> n * p < m * p
intros p n m.p, n, m:t
0 < p -> n < m <-> n * p < m * p
rewrite (mul_comm n p), (mul_comm m p).p, n, m:t
0 < p -> n < m <-> p * n < p * m now apply mul_lt_mono_pos_l.
Qed.

Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).forall p n m : t, p < 0 -> n < m <-> p * m < p * n
Proof.forall p n m : t, p < 0 -> n < m <-> p * m < p * n
nzord_induct p.forall n m : t, 0 < 0 -> n < m <-> 0 * m < 0 * n
forall n : t,
0 <= n ->
(forall n0 m : t, n < 0 -> n0 < m <-> n * m < n * n0) ->
forall n0 m : t,
S n < 0 -> n0 < m <-> S n * m < S n * n0
forall n : t,
n < 0 ->
(forall n0 m : t,
 S n < 0 -> n0 < m <-> S n * m < S n * n0) ->
forall n0 m : t, n < 0 -> n0 < m <-> n * m < n * n0
-forall n m : t, 0 < 0 -> n < m <-> 0 * m < 0 * n order.
-forall n : t,
0 <= n ->
(forall n0 m : t, n < 0 -> n0 < m <-> n * m < n * n0) ->
forall n0 m : t,
S n < 0 -> n0 < m <-> S n * m < S n * n0 intros p Hp _ n m Hp'.p:t
Hp:0 <= p
n, m:t
Hp':S p < 0
n < m <-> S p * m < S p * n apply lt_succ_l in Hp'.p:t
Hp:0 <= p
n, m:t
Hp':p < 0
n < m <-> S p * m < S p * n order.
-forall n : t,
n < 0 ->
(forall n0 m : t,
 S n < 0 -> n0 < m <-> S n * m < S n * n0) ->
forall n0 m : t, n < 0 -> n0 < m <-> n * m < n * n0 intros p Hp IH n m _.p:t
Hp:p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n apply le_succ_l in Hp.p:t
Hp:S p <= 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n
  le_elim Hp.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n
p:t
Hp:S p == 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n
  +p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n assert (LR : forall n m, n < m -> p * m < p * n).p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
n < m <-> p * m < p * n
    *p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0 intros n1 m1 H.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
p * m1 < p * n1 apply (le_lt_add_lt n1 m1).p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
n1 <= m1
p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
p * m1 + m1 < p * n1 + n1
      --p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
n1 <= m1 now apply lt_le_incl.
      --p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
p * m1 + m1 < p * n1 + n1 rewrite <- 2 mul_succ_l.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m, n1, m1:t
H:n1 < m1
S p * m1 < S p * n1 now rewrite <- IH.
    *p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
n < m <-> p * m < p * n split; intros H.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:n < m
p * m < p * n
p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
n < m
      --p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:n < m
p * m < p * n now apply LR.
      --p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
n < m destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
EQ:n == m
n < m
p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
GT:m < n
n < m
         ++p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
EQ:n == m
n < m rewrite EQ in H.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * m
EQ:n == m
n < m order.
         ++p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
GT:m < n
n < m apply LR in GT.p:t
Hp:S p < 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
LR:forall n0 m0 : t, n0 < m0 -> p * m0 < p * n0
H:p * m < p * n
GT:p * n < p * m
n < m order.
  +p:t
Hp:S p == 0
IH:forall n0 m0 : t,
S p < 0 -> n0 < m0 <-> S p * m0 < S p * n0
n, m:t
n < m <-> p * m < p * n rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl.
Qed.

Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p).forall p n m : t, p < 0 -> n < m <-> m * p < n * p
Proof.forall p n m : t, p < 0 -> n < m <-> m * p < n * p
intros p n m.p, n, m:t
p < 0 -> n < m <-> m * p < n * p
rewrite (mul_comm n p), (mul_comm m p).p, n, m:t
p < 0 -> n < m <-> p * m < p * n now apply mul_lt_mono_neg_l.
Qed.

Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m.forall n m p : t, 0 <= p -> n <= m -> p * n <= p * m
Proof.forall n m p : t, 0 <= p -> n <= m -> p * n <= p * m
intros n m p H1 H2.n, m, p:t
H1:0 <= p
H2:n <= m
p * n <= p * m le_elim H1.n, m, p:t
H1:0 < p
H2:n <= m
p * n <= p * m
n, m, p:t
H1:0 == p
H2:n <= m
p * n <= p * m
-n, m, p:t
H1:0 < p
H2:n <= m
p * n <= p * m le_elim H2.n, m, p:t
H1:0 < p
H2:n < m
p * n <= p * m
n, m, p:t
H1:0 < p
H2:n == m
p * n <= p * m +n, m, p:t
H1:0 < p
H2:n < m
p * n <= p * m apply lt_le_incl.n, m, p:t
H1:0 < p
H2:n < m
p * n < p * m now apply mul_lt_mono_pos_l.
  +n, m, p:t
H1:0 < p
H2:n == m
p * n <= p * m apply eq_le_incl; now rewrite H2.
-n, m, p:t
H1:0 == p
H2:n <= m
p * n <= p * m apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l.
Qed.

Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n.forall n m p : t, p <= 0 -> n <= m -> p * m <= p * n
Proof.forall n m p : t, p <= 0 -> n <= m -> p * m <= p * n
intros n m p H1 H2.n, m, p:t
H1:p <= 0
H2:n <= m
p * m <= p * n le_elim H1.n, m, p:t
H1:p < 0
H2:n <= m
p * m <= p * n
n, m, p:t
H1:p == 0
H2:n <= m
p * m <= p * n
-n, m, p:t
H1:p < 0
H2:n <= m
p * m <= p * n le_elim H2.n, m, p:t
H1:p < 0
H2:n < m
p * m <= p * n
n, m, p:t
H1:p < 0
H2:n == m
p * m <= p * n +n, m, p:t
H1:p < 0
H2:n < m
p * m <= p * n apply lt_le_incl.n, m, p:t
H1:p < 0
H2:n < m
p * m < p * n now apply mul_lt_mono_neg_l.
  +n, m, p:t
H1:p < 0
H2:n == m
p * m <= p * n apply eq_le_incl; now rewrite H2.
-n, m, p:t
H1:p == 0
H2:n <= m
p * m <= p * n apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l.
Qed.

Theorem mul_le_mono_nonneg_r : forall n m p, 0 <= p -> n <= m -> n * p <= m * p.forall n m p : t, 0 <= p -> n <= m -> n * p <= m * p
Proof.forall n m p : t, 0 <= p -> n <= m -> n * p <= m * p
intros n m p H1 H2;
rewrite (mul_comm n p), (mul_comm m p); now apply mul_le_mono_nonneg_l.
Qed.

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

Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).forall n m p : t, p ~= 0 -> p * n == p * m <-> n == m
Proof.forall n m p : t, p ~= 0 -> p * n == p * m <-> n == m
intros n m p Hp; split; intro H; [|now f_equiv].n, m, p:t
Hp:p ~= 0
H:p * n == p * m
n == m
apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp];
 destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.n, m, p:t
Hp:p < 0
H:p * n == p * m
LT:n < m
n == m
n, m, p:t
Hp:p < 0
H:p * n == p * m
GT:m < n
n == m
n, m, p:t
Hp:0 < p
H:p * n == p * m
LT:n < m
n == m
n, m, p:t
Hp:0 < p
H:p * n == p * m
GT:m < n
n == m
-n, m, p:t
Hp:p < 0
H:p * n == p * m
LT:n < m
n == m apply (mul_lt_mono_neg_l p) in LT; order.
-n, m, p:t
Hp:p < 0
H:p * n == p * m
GT:m < n
n == m apply (mul_lt_mono_neg_l p) in GT; order.
-n, m, p:t
Hp:0 < p
H:p * n == p * m
LT:n < m
n == m apply (mul_lt_mono_pos_l p) in LT; order.
-n, m, p:t
Hp:0 < p
H:p * n == p * m
GT:m < n
n == m apply (mul_lt_mono_pos_l p) in GT; order.
Qed.

Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m).forall n m p : t, p ~= 0 -> n * p == m * p <-> n == m
Proof.forall n m p : t, p ~= 0 -> n * p == m * p <-> n == m
intros n m p.n, m, p:t
p ~= 0 -> n * p == m * p <-> n == m rewrite (mul_comm n p), (mul_comm m p); apply mul_cancel_l.
Qed.

Theorem mul_id_l : forall n m, m ~= 0 -> (n * m == m <-> n == 1).forall n m : t, m ~= 0 -> n * m == m <-> n == 1
Proof.forall n m : t, m ~= 0 -> n * m == m <-> n == 1
intros n m H.n, m:t
H:m ~= 0
n * m == m <-> n == 1
stepl (n * m == 1 * m) by now rewrite mul_1_l.n, m:t
H:m ~= 0
n * m == 1 * m <-> n == 1 now apply mul_cancel_r.
Qed.

Theorem mul_id_r : forall n m, n ~= 0 -> (n * m == n <-> m == 1).forall n m : t, n ~= 0 -> n * m == n <-> m == 1
Proof.forall n m : t, n ~= 0 -> n * m == n <-> m == 1
intros n m; rewrite mul_comm; apply mul_id_l.
Qed.

Theorem mul_le_mono_pos_l : forall n m p, 0 < p -> (n <= m <-> p * n <= p * m).forall n m p : t, 0 < p -> n <= m <-> p * n <= p * m
Proof.forall n m p : t, 0 < p -> n <= m <-> p * n <= p * m
intros n m p H; do 2 rewrite lt_eq_cases.n, m, p:t
H:0 < p
n < m \/ n == m <-> p * n < p * m \/ p * n == p * m
rewrite (mul_lt_mono_pos_l p n m) by assumption.n, m, p:t
H:0 < p
p * n < p * m \/ n == m <->
p * n < p * m \/ p * n == p * m
now rewrite -> (mul_cancel_l n m p) by
(intro H1; rewrite H1 in H; false_hyp H lt_irrefl).
Qed.

Theorem mul_le_mono_pos_r : forall n m p, 0 < p -> (n <= m <-> n * p <= m * p).forall n m p : t, 0 < p -> n <= m <-> n * p <= m * p
Proof.forall n m p : t, 0 < p -> n <= m <-> n * p <= m * p
intros n m p.n, m, p:t
0 < p -> n <= m <-> n * p <= m * p rewrite (mul_comm n p), (mul_comm m p); apply mul_le_mono_pos_l.
Qed.

Theorem mul_le_mono_neg_l : forall n m p, p < 0 -> (n <= m <-> p * m <= p * n).forall n m p : t, p < 0 -> n <= m <-> p * m <= p * n
Proof.forall n m p : t, p < 0 -> n <= m <-> p * m <= p * n
intros n m p H; do 2 rewrite lt_eq_cases.n, m, p:t
H:p < 0
n < m \/ n == m <-> p * m < p * n \/ p * m == p * n
rewrite (mul_lt_mono_neg_l p n m); [| assumption].n, m, p:t
H:p < 0
p * m < p * n \/ n == m <->
p * m < p * n \/ p * m == p * n
rewrite -> (mul_cancel_l m n p)
 by (intro H1; rewrite H1 in H; false_hyp H lt_irrefl).n, m, p:t
H:p < 0
p * m < p * n \/ n == m <-> p * m < p * n \/ m == n
now setoid_replace (n == m) with (m == n) by (split; now intro).
Qed.

Theorem mul_le_mono_neg_r : forall n m p, p < 0 -> (n <= m <-> m * p <= n * p).forall n m p : t, p < 0 -> n <= m <-> m * p <= n * p
Proof.forall n m p : t, p < 0 -> n <= m <-> m * p <= n * p
intros n m p.n, m, p:t
p < 0 -> n <= m <-> m * p <= n * p rewrite (mul_comm n p), (mul_comm m p); apply mul_le_mono_neg_l.
Qed.

Theorem mul_lt_mono_nonneg :
  forall n m p q, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.forall n m p q : t,
0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q
Proof.forall n m p q : t,
0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q
intros n m p q H1 H2 H3 H4.n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
n * p < m * q
apply le_lt_trans with (m * p).n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
n * p <= m * p
n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
m * p < m * q
-n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
n * p <= m * p apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
-n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
m * p < m * q apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n].
Qed.

(* There are still many variants of the theorem above. One can assume 0 < n
or 0 < p or n <= m or p <= q. *)

Theorem mul_le_mono_nonneg :
  forall n m p q, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.forall n m p q : t,
0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q
Proof.forall n m p q : t,
0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q
intros n m p q H1 H2 H3 H4.n, m, p, q:t
H1:0 <= n
H2:n <= m
H3:0 <= p
H4:p <= q
n * p <= m * q
le_elim H2; le_elim H4.n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
n * p <= m * q
n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p == q
n * p <= m * q
n, m, p, q:t
H1:0 <= n
H2:n == m
H3:0 <= p
H4:p < q
n * p <= m * q
n, m, p, q:t
H1:0 <= n
H2:n == m
H3:0 <= p
H4:p == q
n * p <= m * q
-n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p < q
n * p <= m * q apply lt_le_incl; now apply mul_lt_mono_nonneg.
-n, m, p, q:t
H1:0 <= n
H2:n < m
H3:0 <= p
H4:p == q
n * p <= m * q rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
-n, m, p, q:t
H1:0 <= n
H2:n == m
H3:0 <= p
H4:p < q
n * p <= m * q rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl].
-n, m, p, q:t
H1:0 <= n
H2:n == m
H3:0 <= p
H4:p == q
n * p <= m * q rewrite H2; rewrite H4; now apply eq_le_incl.
Qed.

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

Theorem mul_neg_neg : 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_lt_mono_neg_r.
Qed.

Theorem mul_pos_neg : 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_lt_mono_neg_r.
Qed.

Theorem mul_neg_pos : 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_pos_neg.
Qed.

Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n*m.forall n m : t, 0 <= n -> 0 <= m -> 0 <= n * m
Proof.forall n m : t, 0 <= n -> 0 <= m -> 0 <= n * m
intros.n, m:t
H:0 <= n
H0:0 <= m
0 <= n * m rewrite <- (mul_0_l m).n, m:t
H:0 <= n
H0:0 <= m
0 * m <= n * m apply mul_le_mono_nonneg; order.
Qed.

Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m).forall n m : t, 0 < n -> 0 < n * m <-> 0 < m
Proof.forall n m : t, 0 < n -> 0 < n * m <-> 0 < m
intros n m Hn.n, m:t
Hn:0 < n
0 < n * m <-> 0 < m rewrite <- (mul_0_r n) at 1.n, m:t
Hn:0 < n
n * 0 < n * m <-> 0 < m
 symmetry.n, m:t
Hn:0 < n
0 < m <-> n * 0 < n * m now apply mul_lt_mono_pos_l.
Qed.

Theorem mul_pos_cancel_r : forall n m, 0 < m -> (0 < n*m <-> 0 < n).forall n m : t, 0 < m -> 0 < n * m <-> 0 < n
Proof.forall n m : t, 0 < m -> 0 < n * m <-> 0 < n
intros n m Hn.n, m:t
Hn:0 < m
0 < n * m <-> 0 < n rewrite <- (mul_0_l m) at 1.n, m:t
Hn:0 < m
0 * m < n * m <-> 0 < n
 symmetry.n, m:t
Hn:0 < m
0 < n <-> 0 * m < n * m now apply mul_lt_mono_pos_r.
Qed.

Theorem mul_nonneg_cancel_l : forall n m, 0 < n -> (0 <= n*m <-> 0 <= m).forall n m : t, 0 < n -> 0 <= n * m <-> 0 <= m
Proof.forall n m : t, 0 < n -> 0 <= n * m <-> 0 <= m
intros n m Hn.n, m:t
Hn:0 < n
0 <= n * m <-> 0 <= m rewrite <- (mul_0_r n) at 1.n, m:t
Hn:0 < n
n * 0 <= n * m <-> 0 <= m
 symmetry.n, m:t
Hn:0 < n
0 <= m <-> n * 0 <= n * m now apply mul_le_mono_pos_l.
Qed.

Theorem mul_nonneg_cancel_r : forall n m, 0 < m -> (0 <= n*m <-> 0 <= n).forall n m : t, 0 < m -> 0 <= n * m <-> 0 <= n
Proof.forall n m : t, 0 < m -> 0 <= n * m <-> 0 <= n
intros n m Hn.n, m:t
Hn:0 < m
0 <= n * m <-> 0 <= n rewrite <- (mul_0_l m) at 1.n, m:t
Hn:0 < m
0 * m <= n * m <-> 0 <= n
 symmetry.n, m:t
Hn:0 < m
0 <= n <-> 0 * m <= n * m now apply mul_le_mono_pos_r.
Qed.

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

Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0.forall n m : t, n * m == 0 <-> n == 0 \/ m == 0
Proof.forall n m : t, n * m == 0 <-> n == 0 \/ m == 0
intros n m; split.n, m:t
n * m == 0 -> n == 0 \/ m == 0
n, m:t
n == 0 \/ m == 0 -> n * m == 0
-n, m:t
n * m == 0 -> n == 0 \/ m == 0 intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
    destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
    try (now right); try (now left).n, m:t
H:n * m == 0
H1:n < 0
H2:m < 0
n == 0 \/ m == 0
n, m:t
H:n * m == 0
H1:n < 0
H2:0 < m
n == 0 \/ m == 0
n, m:t
H:n * m == 0
H1:0 < n
H2:m < 0
n == 0 \/ m == 0
n, m:t
H:n * m == 0
H1:0 < n
H2:0 < m
n == 0 \/ m == 0
  +n, m:t
H:n * m == 0
H1:n < 0
H2:m < 0
n == 0 \/ m == 0 exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |].
  +n, m:t
H:n * m == 0
H1:n < 0
H2:0 < m
n == 0 \/ m == 0 exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |].
  +n, m:t
H:n * m == 0
H1:0 < n
H2:m < 0
n == 0 \/ m == 0 exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |].
  +n, m:t
H:n * m == 0
H1:0 < n
H2:0 < m
n == 0 \/ m == 0 exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |].
-n, m:t
n == 0 \/ m == 0 -> n * m == 0 intros [H | H].n, m:t
H:n == 0
n * m == 0
n, m:t
H:m == 0
n * m == 0 +n, m:t
H:n == 0
n * m == 0 now rewrite H, mul_0_l. +n, m:t
H:m == 0
n * m == 0 now rewrite H, mul_0_r.
Qed.

Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.forall n m : t, n ~= 0 /\ m ~= 0 <-> n * m ~= 0
Proof.forall n m : t, n ~= 0 /\ m ~= 0 <-> n * m ~= 0
intros n m; split; intro H.n, m:t
H:n ~= 0 /\ m ~= 0
n * m ~= 0
n, m:t
H:n * m ~= 0
n ~= 0 /\ m ~= 0
-n, m:t
H:n ~= 0 /\ m ~= 0
n * m ~= 0 intro H1; apply eq_mul_0 in H1.n, m:t
H:n ~= 0 /\ m ~= 0
H1:n == 0 \/ m == 0
False tauto.
-n, m:t
H:n * m ~= 0
n ~= 0 /\ m ~= 0 split; intro H1; rewrite H1 in H;
    (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H.
Qed.

Theorem eq_square_0 : forall n, n * n == 0 <-> n == 0.forall n : t, n * n == 0 <-> n == 0
Proof.forall n : t, n * n == 0 <-> n == 0
intro n; rewrite eq_mul_0; tauto.
Qed.

Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0.forall n m : t, n * m == 0 -> m ~= 0 -> n == 0
Proof.forall n m : t, n * m == 0 -> m ~= 0 -> n == 0
intros n m H1 H2.n, m:t
H1:n * m == 0
H2:m ~= 0
n == 0 apply eq_mul_0 in H1.n, m:t
H1:n == 0 \/ m == 0
H2:m ~= 0
n == 0 destruct H1 as [H1 | H1].n, m:t
H1:n == 0
H2:m ~= 0
n == 0
n, m:t
H1:m == 0
H2:m ~= 0
n == 0
-n, m:t
H1:n == 0
H2:m ~= 0
n == 0 assumption. -n, m:t
H1:m == 0
H2:m ~= 0
n == 0 false_hyp H1 H2.
Qed.

Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0.forall n m : t, n * m == 0 -> n ~= 0 -> m == 0
Proof.forall n m : t, n * m == 0 -> n ~= 0 -> m == 0
intros n m H1 H2; apply eq_mul_0 in H1.n, m:t
H1:n == 0 \/ m == 0
H2:n ~= 0
m == 0 destruct H1 as [H1 | H1].n, m:t
H1:n == 0
H2:n ~= 0
m == 0
n, m:t
H1:m == 0
H2:n ~= 0
m == 0
-n, m:t
H1:n == 0
H2:n ~= 0
m == 0 false_hyp H1 H2. -n, m:t
H1:m == 0
H2:n ~= 0
m == 0 assumption.
Qed.

Some alternative names:

Definition mul_eq_0 := eq_mul_0.
Definition mul_eq_0_l := eq_mul_0_l.
Definition 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).n, m:t
0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0
Proof.n, m:t
0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0
split; [intro H | intros [[H1 H2] | [H1 H2]]].n, m:t
H:0 < n * m
0 < n /\ 0 < m \/ m < 0 /\ n < 0
n, m:t
H1:0 < n
H2:0 < m
0 < n * m
n, m:t
H1:m < 0
H2:n < 0
0 < n * m
-n, m:t
H:0 < n * m
0 < n /\ 0 < m \/ m < 0 /\ n < 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:0 < n * m
H1:n < 0
H2:0 < m
0 < n /\ 0 < m \/ m < 0 /\ n < 0
n, m:t
H:0 < n * m
H1:0 < n
H2:m < 0
0 < n /\ 0 < m \/ m < 0 /\ n < 0
  +n, m:t
H:0 < n * m
H1:n < 0
H2:0 < m
0 < n /\ 0 < m \/ m < 0 /\ n < 0 assert (H3 : n * m < 0) by now apply mul_neg_pos.n, m:t
H:0 < n * m
H1:n < 0
H2:0 < m
H3:n * m < 0
0 < n /\ 0 < m \/ m < 0 /\ n < 0
    exfalso; now apply (lt_asymm (n * m) 0).
  +n, m:t
H:0 < n * m
H1:0 < n
H2:m < 0
0 < n /\ 0 < m \/ m < 0 /\ n < 0 assert (H3 : n * m < 0) by now apply mul_pos_neg.n, m:t
H:0 < n * m
H1:0 < n
H2:m < 0
H3:n * m < 0
0 < n /\ 0 < m \/ m < 0 /\ n < 0
    exfalso; now apply (lt_asymm (n * m) 0).
-n, m:t
H1:0 < n
H2:0 < m
0 < n * m now apply mul_pos_pos. -n, m:t
H1:m < 0
H2:n < 0
0 < n * m now apply mul_neg_neg.
Qed.

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

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

(* The converse theorems require nonnegativity (or nonpositivity) of the
other variable *)

Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m.forall n m : t, 0 <= m -> n * n < m * m -> n < m
Proof.forall n m : t, 0 <= m -> n * n < m * m -> n < m
intros n m H1 H2.n, m:t
H1:0 <= m
H2:n * n < m * m
n < m destruct (lt_ge_cases n 0).n, m:t
H1:0 <= m
H2:n * n < m * m
H:n < 0
n < m
n, m:t
H1:0 <= m
H2:n * n < m * m
H:0 <= n
n < m
-n, m:t
H1:0 <= m
H2:n * n < m * m
H:n < 0
n < m now apply lt_le_trans with 0.
-n, m:t
H1:0 <= m
H2:n * n < m * m
H:0 <= n
n < m destruct (lt_ge_cases n m) as [LT|LE]; trivial.n, m:t
H1:0 <= m
H2:n * n < m * m
H:0 <= n
LE:m <= n
n < m
  apply square_le_mono_nonneg in LE; order.
Qed.

Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m.forall n m : t, 0 <= m -> n * n <= m * m -> n <= m
Proof.forall n m : t, 0 <= m -> n * n <= m * m -> n <= m
intros n m H1 H2.n, m:t
H1:0 <= m
H2:n * n <= m * m
n <= m destruct (lt_ge_cases n 0).n, m:t
H1:0 <= m
H2:n * n <= m * m
H:n < 0
n <= m
n, m:t
H1:0 <= m
H2:n * n <= m * m
H:0 <= n
n <= m
-n, m:t
H1:0 <= m
H2:n * n <= m * m
H:n < 0
n <= m apply lt_le_incl; now apply lt_le_trans with 0.
-n, m:t
H1:0 <= m
H2:n * n <= m * m
H:0 <= n
n <= m destruct (le_gt_cases n m) as [LE|LT]; trivial.n, m:t
H1:0 <= m
H2:n * n <= m * m
H:0 <= n
LT:m < n
n <= m
  apply square_lt_mono_nonneg in LT; order.
Qed.

Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m.forall n m : t, n < m -> 1 + 2 * n < 2 * m
Proof.forall n m : t, n < m -> 1 + 2 * n < 2 * m
intros n m.n, m:t
n < m -> 1 + 2 * n < 2 * m rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two).n, m:t
2 * S n <= 2 * m -> 1 + 2 * n < 2 * m
n, m:t
0 < 2
-n, m:t
2 * S n <= 2 * m -> 1 + 2 * n < 2 * m rewrite two_succ.n, m:t
S 1 * S n <= S 1 * m -> 1 + S 1 * n < S 1 * m nzsimpl.n, m:t
S (S (n + n)) <= m + m -> S (n + n) < m + m now rewrite le_succ_l.
-n, m:t
0 < 2 order'.
Qed.

Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b.forall a b : t, 1 < a -> 1 < b -> a + b <= a * b
Proof.forall a b : t, 1 < a -> 1 < b -> a + b <= a * b
 assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)).forall a b : t,
0 < a -> 0 < b -> S a + S b <= S a * S b
AUX:forall a b : t, 0 < a -> 0 < b -> S a + S b <= S a * S b
forall a b : t, 1 < a -> 1 < b -> a + b <= a * b
 -forall a b : t,
0 < a -> 0 < b -> S a + S b <= S a * S b intros a b Ha Hb.a, b:t
Ha:0 < a
Hb:0 < b
S a + S b <= S a * S b
   nzsimpl.a, b:t
Ha:0 < a
Hb:0 < b
S (S (a + b)) <= S (a * b + b + a) rewrite <- succ_le_mono.a, b:t
Ha:0 < a
Hb:0 < b
S (a + b) <= a * b + b + a apply le_succ_l.a, b:t
Ha:0 < a
Hb:0 < b
a + b < a * b + b + a
   rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b).a, b:t
Ha:0 < a
Hb:0 < b
0 + (a + b) < a * b + (a + b)
   apply add_lt_mono_r.a, b:t
Ha:0 < a
Hb:0 < b
0 < a * b
   now apply mul_pos_pos.
 -AUX:forall a b : t, 0 < a -> 0 < b -> S a + S b <= S a * S b
forall a b : t, 1 < a -> 1 < b -> a + b <= a * b intros a b Ha Hb.AUX:forall a0 b0 : t, 0 < a0 -> 0 < b0 -> S a0 + S b0 <= S a0 * S b0
a, b:t
Ha:1 < a
Hb:1 < b
a + b <= a * b
   assert (Ha' := lt_succ_pred 1 a Ha).AUX:forall a0 b0 : t, 0 < a0 -> 0 < b0 -> S a0 + S b0 <= S a0 * S b0
a, b:t
Ha:1 < a
Hb:1 < b
Ha':S (P a) == a
a + b <= a * b
   assert (Hb' := lt_succ_pred 1 b Hb).AUX:forall a0 b0 : t, 0 < a0 -> 0 < b0 -> S a0 + S b0 <= S a0 * S b0
a, b:t
Ha:1 < a
Hb:1 < b
Ha':S (P a) == a
Hb':S (P b) == b
a + b <= a * b
   rewrite <- Ha', <- Hb'.AUX:forall a0 b0 : t, 0 < a0 -> 0 < b0 -> S a0 + S b0 <= S a0 * S b0
a, b:t
Ha:1 < a
Hb:1 < b
Ha':S (P a) == a
Hb':S (P b) == b
S (P a) + S (P b) <= S (P a) * S (P b) apply AUX; rewrite succ_lt_mono, <- one_succ; order.
Qed.

A few results about squares

Lemma square_nonneg : forall a, 0 <= a * a.forall a : t, 0 <= a * a
Proof.forall a : t, 0 <= a * a
 intros.a:t
0 <= a * a rewrite <- (mul_0_r a).a:t
a * 0 <= a * a destruct (le_gt_cases a 0).a:t
H:a <= 0
a * 0 <= a * a
a:t
H:0 < a
a * 0 <= a * a
 -a:t
H:a <= 0
a * 0 <= a * a now apply mul_le_mono_nonpos_l.
 -a:t
H:0 < a
a * 0 <= a * a apply mul_le_mono_nonneg_l; order.
Qed.

Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b.forall a b : t,
0 <= a -> 0 <= b -> b * a + a * b <= a * a + b * b
Proof.forall a b : t,
0 <= a -> 0 <= b -> b * a + a * b <= a * a + b * b
 assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b).forall a b : t,
0 <= a <= b -> b * a + a * b <= a * a + b * b
AUX:forall a b : t, 0 <= a <= b -> b * a + a * b <= a * a + b * b
forall a b : t,
0 <= a -> 0 <= b -> b * a + a * b <= a * a + b * b
 -forall a b : t,
0 <= a <= b -> b * a + a * b <= a * a + b * b intros a b (Ha,H).a, b:t
Ha:0 <= a
H:a <= b
b * a + a * b <= a * a + b * b
   destruct (le_exists_sub _ _ H) as (d & EQ & Hd).a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
b * a + a * b <= a * a + b * b
   rewrite EQ.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
(d + a) * a + a * (d + a) <= a * a + (d + a) * (d + a)
   rewrite 2 mul_add_distr_r.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
d * a + a * a + a * (d + a) <=
a * a + (d * (d + a) + a * (d + a))
   rewrite !add_assoc.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
d * a + a * a + a * (d + a) <=
a * a + d * (d + a) + a * (d + a) apply add_le_mono_r.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
d * a + a * a <= a * a + d * (d + a)
   rewrite add_comm.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
a * a + d * a <= a * a + d * (d + a) apply add_le_mono_l.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
d * a <= d * (d + a)
   apply mul_le_mono_nonneg_l; trivial.a, b:t
Ha:0 <= a
H:a <= b
d:t
EQ:b == d + a
Hd:0 <= d
a <= d + a order.
 -AUX:forall a b : t, 0 <= a <= b -> b * a + a * b <= a * a + b * b
forall a b : t,
0 <= a -> 0 <= b -> b * a + a * b <= a * a + b * b intros a b Ha Hb.AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
b * a + a * b <= a * a + b * b
   destruct (le_gt_cases a b).AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
H:a <= b
b * a + a * b <= a * a + b * b
AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < a
b * a + a * b <= a * a + b * b
   +AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
H:a <= b
b * a + a * b <= a * a + b * b apply AUX; split; order.
   +AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < a
b * a + a * b <= a * a + b * b rewrite (add_comm (b*a)), (add_comm (a*a)).AUX:forall a0 b0 : t, 0 <= a0 <= b0 -> b0 * a0 + a0 * b0 <= a0 * a0 + b0 * b0
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < a
a * b + b * a <= b * b + a * a
     apply AUX; split; order.
Qed.

Lemma add_square_le : forall a b, 0<=a -> 0<=b ->
 a*a + b*b <= (a+b)*(a+b).forall a b : t,
0 <= a -> 0 <= b -> a * a + b * b <= (a + b) * (a + b)
Proof.forall a b : t,
0 <= a -> 0 <= b -> a * a + b * b <= (a + b) * (a + b)
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + b * b <= (a + b) * (a + b)
 rewrite mul_add_distr_r, !mul_add_distr_l.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + b * b <= a * a + a * b + (b * a + b * b)
 rewrite add_assoc.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + b * b <= a * a + a * b + b * a + b * b
 apply add_le_mono_r.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a <= a * a + a * b + b * a
 rewrite <- add_assoc.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a <= a * a + (a * b + b * a)
 rewrite <- (add_0_r (a*a)) at 1.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + 0 <= a * a + (a * b + b * a)
 apply add_le_mono_l.a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a * b + b * a
 apply add_nonneg_nonneg; now apply mul_nonneg_nonneg.
Qed.

Lemma square_add_le : forall a b, 0<=a -> 0<=b ->
 (a+b)*(a+b) <= 2*(a*a + b*b).forall a b : t,
0 <= a ->
0 <= b -> (a + b) * (a + b) <= 2 * (a * a + b * b)
Proof.forall a b : t,
0 <= a ->
0 <= b -> (a + b) * (a + b) <= 2 * (a * a + b * b)
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
(a + b) * (a + b) <= 2 * (a * a + b * b)
 rewrite !mul_add_distr_l, !mul_add_distr_r.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + b * a + (a * b + b * b) <=
2 * (a * a) + 2 * (b * b) nzsimpl'.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + b * a + (a * b + b * b) <=
a * a + a * a + (b * b + b * b)
 rewrite <- !add_assoc.a, b:t
Ha:0 <= a
Hb:0 <= b
a * a + (b * a + (a * b + b * b)) <=
a * a + (a * a + (b * b + b * b)) apply add_le_mono_l.a, b:t
Ha:0 <= a
Hb:0 <= b
b * a + (a * b + b * b) <= a * a + (b * b + b * b)
 rewrite !add_assoc.a, b:t
Ha:0 <= a
Hb:0 <= b
b * a + a * b + b * b <= a * a + b * b + b * b apply add_le_mono_r.a, b:t
Ha:0 <= a
Hb:0 <= b
b * a + a * b <= a * a + b * b
 apply crossmul_le_addsquare; order.
Qed.

Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b ->
 2*2*a*b <= (a+b)*(a+b).forall a b : t,
0 <= a -> 0 <= b -> 2 * 2 * a * b <= (a + b) * (a + b)
Proof.forall a b : t,
0 <= a -> 0 <= b -> 2 * 2 * a * b <= (a + b) * (a + b)
 intros.a, b:t
H:0 <= a
H0:0 <= b
2 * 2 * a * b <= (a + b) * (a + b)
 nzsimpl'.a, b:t
H:0 <= a
H0:0 <= b
(a + a + a + a) * b <= (a + b) * (a + b)
 rewrite !mul_add_distr_l, !mul_add_distr_r.a, b:t
H:0 <= a
H0:0 <= b
a * b + a * b + a * b + a * b <=
a * a + b * a + (a * b + b * b)
 rewrite (add_comm _ (b*b)), add_assoc.a, b:t
H:0 <= a
H0:0 <= b
a * b + a * b + a * b + a * b <=
a * a + b * a + b * b + a * b
 apply add_le_mono_r.a, b:t
H:0 <= a
H0:0 <= b
a * b + a * b + a * b <= a * a + b * a + b * b
 rewrite (add_shuffle0 (a*a)), (mul_comm b a).a, b:t
H:0 <= a
H0:0 <= b
a * b + a * b + a * b <= a * a + b * b + a * b
 apply add_le_mono_r.a, b:t
H:0 <= a
H0:0 <= b
a * b + a * b <= a * a + b * b
 rewrite (mul_comm a b) at 1.a, b:t
H:0 <= a
H0:0 <= b
b * a + a * b <= a * a + b * b
 now apply crossmul_le_addsquare.
Qed.

End NZMulOrderProp.