(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   lemmas.
   Some nice lemmas, mostly about le, lt, and mult.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Global Set Asymmetric Patterns.

Require Import ZArith.
Require Import EqNat.

Lemma predminus1 : forall n : nat, pred n = n - 1.
Proof.
(* Goal: forall n : nat, or (@eq nat n O) (or (@eq nat n (S O)) (gt n (S O))) *)
   intro n. case n.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. reflexivity.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intro m. rewrite <- minus_n_O. reflexivity.
Qed.

Lemma le_mult_l : forall p q : nat, p <= q -> forall r : nat, r * p <= r * q.
Proof.
(* Goal: forall (p q : nat) (_ : le p q) (r : nat), le (Init.Nat.mul p r) (Init.Nat.mul q r) *)
   intros p q H.
(* Goal: forall (p q r : Z) (_ : Z.lt Z0 r) (_ : Z.le p q), Z.le (Z.mul r p) (Z.mul r q) *)
   simple induction r.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: forall (n : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul q n)), le (Init.Nat.mul p (S n)) (Init.Nat.mul q (S n)) *)
   intros r1 IHr1.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: le (Init.Nat.add (Init.Nat.mul p r1) p) (Init.Nat.add (Init.Nat.mul q r1) q) *)
   apply plus_le_compat.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma lt_plus_plus : forall n m p q : nat, n < m -> p < q -> n + p < m + q.
Proof.
(* Goal: forall (n m p q : nat) (_ : lt n m) (_ : lt p q), lt (Init.Nat.add n p) (Init.Nat.add m q) *)
   intros n m p q H H0.
(* Goal: lt (Init.Nat.add n p) (Init.Nat.add m q) *)
   elim H; simpl in |- *; auto with arith.
Qed.

Lemma lt_mult_l :
 forall p q : nat, p < q -> forall r : nat, S r * p < S r * q.
Proof.
(* Goal: forall (p q : nat) (_ : le p q) (r : nat), le (Init.Nat.mul p r) (Init.Nat.mul q r) *)
   intros p q H.
(* Goal: forall (p q r : Z) (_ : Z.lt Z0 r) (_ : Z.le p q), Z.le (Z.mul r p) (Z.mul r q) *)
   simple induction r.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall _ : @eq nat (Init.Nat.add q O) (S O), and (@eq nat (S O) (S O)) (@eq nat q (S O)) *)
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S (S n)) q) (S O)), and (@eq nat (S (S n)) (S O)) (@eq nat q (S O)) *)
   rewrite <- plus_n_O.
(* Goal: forall _ : @eq nat (Init.Nat.add q O) (S O), and (@eq nat (S O) (S O)) (@eq nat q (S O)) *)
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S (S n)) q) (S O)), and (@eq nat (S (S n)) (S O)) (@eq nat q (S O)) *)
   rewrite <- plus_n_O.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul q n)), le (Init.Nat.mul p (S n)) (Init.Nat.mul q (S n)) *)
   intros r1 IHr1.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: lt (Init.Nat.add p (Init.Nat.add p (Init.Nat.mul r1 p))) (Init.Nat.add q (Init.Nat.add q (Init.Nat.mul r1 q))) *)
   apply lt_plus_plus.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma le_mult_r : forall p q : nat, p <= q -> forall r : nat, p * r <= q * r.
Proof.
(* Goal: forall (p q : nat) (_ : le p q) (r : nat), le (Init.Nat.mul p r) (Init.Nat.mul q r) *)
   intros p q H.
(* Goal: forall (p q r : Z) (_ : Z.lt Z0 r) (_ : Z.le p q), Z.le (Z.mul r p) (Z.mul r q) *)
   simple induction r.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: le (Init.Nat.mul p O) (Init.Nat.mul q O) *)
(* Goal: forall (n : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul q n)), le (Init.Nat.mul p (S n)) (Init.Nat.mul q (S n)) *)
   rewrite <- (mult_n_O p).
(* Goal: le O (Init.Nat.mul q O) *)
(* Goal: forall (n : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul q n)), le (Init.Nat.mul p (S n)) (Init.Nat.mul q (S n)) *)
   rewrite <- (mult_n_O q).
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: forall (n : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul q n)), le (Init.Nat.mul p (S n)) (Init.Nat.mul q (S n)) *)
   intros r1 IHr1.
(* Goal: le (Init.Nat.mul p (S r1)) (Init.Nat.mul q (S r1)) *)
   rewrite <- (mult_n_Sm p r1).
(* Goal: le (Init.Nat.add (Init.Nat.mul p r1) p) (Init.Nat.mul q (S r1)) *)
   rewrite <- (mult_n_Sm q r1).
(* Goal: le (Init.Nat.add (Init.Nat.mul p r1) p) (Init.Nat.add (Init.Nat.mul q r1) q) *)
   apply plus_le_compat.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma sqrbound : forall p q : nat, p * p <= p * q \/ q * q <= p * q.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: or (le (Init.Nat.mul p p) (Init.Nat.mul p q)) (le (Init.Nat.mul q q) (Init.Nat.mul p q)) *)
   elim (le_or_lt p q).
(* Goal: forall (b : Z) (_ : @eq Z Z0 Z0), or (@eq Z Z0 Z0) (@eq Z b Z0) *)
(* Goal: forall (p : positive) (b : Z) (_ : @eq Z (Z.mul (Zpos p) b) Z0), or (@eq Z (Zpos p) Z0) (@eq Z b Z0) *)
(* Goal: forall (p : positive) (b : Z) (_ : @eq Z (Z.mul (Zneg p) b) Z0), or (@eq Z (Zneg p) Z0) (@eq Z b Z0) *)
   left.
(* Goal: le (Init.Nat.mul (S b1) c) (Init.Nat.mul (S b1) d) *)
(* Goal: @eq nat (Init.Nat.mul (S b1) d) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   apply le_mult_l.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall _ : @eq Z Z0 Z0, or (@eq Z (Zneg p) Z0) (@eq Z Z0 Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zpos p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zpos p0) Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zneg p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zneg p0) Z0) *)
   right.
(* Goal: le (Init.Nat.mul q q) (Init.Nat.mul p q) *)
   apply le_mult_r.
(* Goal: le (Init.Nat.mul (S a1) c) (Init.Nat.mul (S a1) b) *)
   apply lt_le_weak.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma le_n_nm : forall n m : nat, n <= n * S m.
Proof.
(* Goal: forall (n : nat) (_ : gt n (S O)), lt n (Init.Nat.mul n n) *)
   simple induction n.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: forall (n : nat) (_ : forall m : nat, le n (Init.Nat.mul n (S m))) (m : nat), le (S n) (Init.Nat.mul (S n) (S m)) *)
   intros n1 IHn1.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (S (Init.Nat.mul a c)) (S (Init.Nat.add c (Init.Nat.mul a (S c)))) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_n_S.
(* Goal: le n1 (Init.Nat.add m (Init.Nat.mul n1 (S m))) *)
   rewrite (plus_comm m (n1 * S m)).
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add (Init.Nat.mul a c) a) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_plus_trans.
(* Goal: le n1 (Init.Nat.mul n1 (S m)) *)
   apply IHn1.
Qed.

Lemma le_n_mn : forall n m : nat, n <= S m * n.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le n (Init.Nat.mul (S m) n) *)
   rewrite (mult_comm (S m) n).
(* Goal: le n (Nat.mul n (S m)) *)
   apply le_n_nm.
Qed.

Lemma le_n_nn : forall n : nat, n <= n * n.
Proof.
(* Goal: forall n : nat, or (@eq nat n O) (or (@eq nat n (S O)) (gt n (S O))) *)
   intro n. case n.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. apply le_n.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. apply le_n_S. apply le_plus_trans. apply le_n.
Qed.

Lemma lt_n_nm : forall n m : nat, 0 < n -> 1 < m -> n < n * m. 
Proof.
(* Goal: forall (n m : nat) (_ : lt O n) (_ : lt (S O) m), lt n (Init.Nat.mul n m) *)
   intros n m.
(* Goal: or (@eq nat n O) (or (@eq nat n (S O)) (gt n (S O))) *)
   case n. intros. elim (lt_n_O 0). assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro n1. case m. intros. elim (lt_n_O 1). assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro m1. case m1. intros. elim (lt_irrefl 1). assumption.
(* Goal: forall (n : nat) (_ : lt O (S n1)) (_ : lt (S O) (S (S n))), lt (S n1) (Init.Nat.mul (S n1) (S (S n))) *)
   intro m2. elim n1.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. apply lt_n_S. apply lt_O_Sn.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros n2 IH. intros.
(* Goal: lt (S m) (S (Init.Nat.add m (Init.Nat.mul m (S m)))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_n_S.
(* Goal: lt (S n2) (S (Init.Nat.add m2 (S (S (Init.Nat.add m2 (Init.Nat.mul n2 (S (S m2)))))))) *)
   apply lt_trans with (S (S (m2 + n2 * S (S m2)))).
(* Goal: lt (S n2) (S (S (Init.Nat.add m2 (Init.Nat.mul n2 (S (S m2)))))) *)
(* Goal: lt (S (S (Init.Nat.add m2 (Init.Nat.mul n2 (S (S m2)))))) (S (Init.Nat.add m2 (S (S (Init.Nat.add m2 (Init.Nat.mul n2 (S (S m2)))))))) *)
   apply IH.
(* Goal: lt O (S p1) *)
(* Goal: @eq nat (Init.Nat.mul (S p1) q) (Init.Nat.mul (S p1) (S O)) *)
   apply lt_O_Sn.
(* Goal: lt (S m) (S (Init.Nat.add m (Init.Nat.mul m (S m)))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_n_S.
(* Goal: lt O (S p1) *)
(* Goal: @eq nat (Init.Nat.mul (S p1) q) (Init.Nat.mul (S p1) (S O)) *)
   apply lt_O_Sn.
(* Goal: lt (S m) (S (Init.Nat.add m (Init.Nat.mul m (S m)))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_n_S.
(* Goal: lt (S (Nat.add (Init.Nat.mul n2 (S (S m2))) m2)) (Init.Nat.add m2 (S (S (Nat.add (Init.Nat.mul n2 (S (S m2))) m2)))) *)
   rewrite (plus_comm m2).
(* Goal: lt (S (Nat.add (Init.Nat.mul n2 (S (S m2))) m2)) (Init.Nat.add m2 (S (S (Nat.add (Init.Nat.mul n2 (S (S m2))) m2)))) *)
   rewrite (plus_comm m2).
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: lt (S m) (S (Init.Nat.add m (Init.Nat.mul m (S m)))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_n_S.
(* Goal: lt (Nat.add (Init.Nat.mul n2 (S (S m2))) m2) (S (Nat.add (Nat.add (Init.Nat.mul n2 (S (S m2))) m2) m2)) *)
   apply lt_le_trans with (S (n2 * S (S m2) + m2)).
(* Goal: lt (S p2) (S (S p2)) *)
   apply lt_n_Sn.
(* Goal: le (S (Init.Nat.mul a c)) (S (Init.Nat.add c (Init.Nat.mul a (S c)))) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_n_S.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add (Init.Nat.mul a c) a) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_plus_trans.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
Qed.

Lemma sqr_ascend : forall n : nat, n > 1 -> n < n * n.
Proof.
(* Goal: forall (n : nat) (_ : gt n (S O)), lt n (Init.Nat.mul n n) *)
   simple induction n.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt (Init.Nat.mul (Init.Nat.pred O) (Init.Nat.pred O)) (Init.Nat.mul O O) *)
(* Goal: forall (n : nat) (_ : gt (S n) (S O)), lt (Init.Nat.mul (Init.Nat.pred (S n)) (Init.Nat.pred (S n))) (Init.Nat.mul (S n) (S n)) *)
   elim (lt_n_O 1).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : forall _ : gt n (S O), lt n (Init.Nat.mul n n)) (_ : gt (S n) (S O)), lt (S n) (Init.Nat.mul (S n) (S n)) *)
   intros m IHm.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: lt (S m) (Init.Nat.mul (S m) (S m)) *)
   unfold gt in H.
(* Goal: lt (S m) (Init.Nat.mul (S m) (S m)) *)
   unfold lt in H.
(* Goal: lt (S m) (Init.Nat.mul (S m) (S m)) *)
   elim (le_lt_or_eq 1 m).
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: lt (S m) (S (Init.Nat.add m (Init.Nat.mul m (S m)))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_n_S.
(* Goal: lt m (Init.Nat.add m (Init.Nat.mul m (S m))) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   rewrite <- (mult_n_Sm m m).
(* Goal: lt m (Init.Nat.add m (Init.Nat.add (Init.Nat.mul m m) m)) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   rewrite plus_comm.
(* Goal: lt m (Init.Nat.add (Init.Nat.mul m m) m) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_plus_trans.
(* Goal: lt m (Init.Nat.add (Init.Nat.mul m m) m) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply lt_plus_trans.
(* Goal: lt m (Init.Nat.mul m m) *)
(* Goal: forall _ : @eq nat (S O) m, lt (S m) (Init.Nat.mul (S m) (S m)) *)
(* Goal: le (S O) m *)
   apply IHm.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le x y *)
   rewrite <- H0.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (a b c d : nat) (_ : lt a b) (_ : lt c d), lt (Init.Nat.mul a c) (Init.Nat.mul b d) *)
   unfold lt in |- *.
(* Goal: le x (S (Init.Nat.add x n)) *)
   apply le_S.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: le (Init.Nat.add b1 c) b1 *)
(* Goal: @eq nat (Init.Nat.add b1 c) (Init.Nat.add b1 c) *)
   apply le_S_n.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma witness_le : forall x y : nat, (exists q : nat, x + q = y) -> x <= y.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. elim H. intro q. intros.
(* Goal: le x y *)
   rewrite <- H0.
(* Goal: le x (Init.Nat.add x q) *)
   elim q.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   rewrite <- plus_n_O. apply le_n.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. rewrite <- plus_n_Sm. apply le_S. assumption.
Qed.

Lemma le_witness : forall x y : nat, x <= y -> exists q : nat, x + q = y.
Proof.
(* Goal: forall (x y : nat) (_ : le x y), @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) y) *)
   intros x y.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) y) *)
   elim H.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) x) *)
(* Goal: forall (m : nat) (_ : le x m) (_ : @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) m)), @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) (S m)) *)
   split with 0.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
   symmetry  in |- *.
(* Goal: @eq nat x (Init.Nat.add x O) *)
(* Goal: forall (m : nat) (_ : le x m) (_ : @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) m)), @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) (S m)) *)
   apply plus_n_O.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.add x q) (S m)) *)
   case H1.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: @ex nat (fun q : nat => and (@eq nat (Init.Nat.add x q) y) (le (S O) q)) *)
(* Goal: le (S x) y *)
   split with (S x0).
(* Goal: @eq nat (Init.Nat.add x (S x0)) (S m) *)
   replace (x + S x0) with (S (x + x0)).
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: @eq nat (S (Init.Nat.add x x0)) (S m) *)
(* Goal: @eq nat (S (Init.Nat.add x x0)) (Init.Nat.add x (S x0)) *)
   rewrite H2.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   reflexivity.
(* Goal: @eq nat (S (Init.Nat.add x x0)) (Init.Nat.add x (S x0)) *)
   apply plus_n_Sm.
Qed.

Lemma lt_witness :
 forall x y : nat, x < y -> exists q : nat, x + q = y /\ 0 < q.
Proof.
(* Goal: forall (a b c d : nat) (_ : lt a b) (_ : lt c d), lt (Init.Nat.mul a c) (Init.Nat.mul b d) *)
   unfold lt in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: @ex nat (fun q : nat => and (@eq nat (Init.Nat.add x q) y) (le (S O) q)) *)
   elim (le_witness (S x) y).
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: @ex nat (fun q : nat => and (@eq nat (Init.Nat.add x q) y) (le (S O) q)) *)
(* Goal: le (S x) y *)
   split with (S x0).
(* Goal: forall _ : @eq nat q (S O), and (@eq nat (S O) (S O)) (@eq nat q (S O)) *)
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S (S n)) q) (S O)), and (@eq nat (S (S n)) (S O)) (@eq nat q (S O)) *)
   split.
(* Goal: @eq nat (Init.Nat.add x (S x0)) y *)
(* Goal: le (S O) (S x0) *)
(* Goal: le (S x) y *)
   rewrite <- plus_n_Sm.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: le (S (Init.Nat.mul a c)) (S (Init.Nat.add c (Init.Nat.mul a (S c)))) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_n_S.
(* Goal: le O x0 *)
(* Goal: le (S x) y *)
   apply le_O_n.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.


Lemma le_le_mult : forall b a c d : nat, a <= b -> c <= d -> a * c <= b * d.
Proof.
(* Goal: forall (b : Z) (_ : @eq Z (Z.mul (Zneg p) b) Z0), or (@eq Z (Zneg p) Z0) (@eq Z b Z0) *)
   simple induction b.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul O d) *)
(* Goal: forall (n : nat) (_ : forall (a c d : nat) (_ : le a n) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul n d)) (a c d : nat) (_ : le a (S n)) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul (S n) d) *)
   replace a with 0.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: @eq nat O a *)
(* Goal: forall (n : nat) (_ : forall (a c d : nat) (_ : le a n) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul n d)) (a c d : nat) (_ : le a (S n)) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul (S n) d) *)
   apply le_n_O_eq.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : forall (a c d : nat) (_ : le a n) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul n d)) (a c d : nat) (_ : le a (S n)) (_ : le c d), le (Init.Nat.mul a c) (Init.Nat.mul (S n) d) *)
   intros b1 IHb1.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
   elim (le_lt_or_eq a (S b1)).
(* Goal: forall (a b c d : nat) (_ : lt a b) (_ : lt c d), lt (Init.Nat.mul a c) (Init.Nat.mul b d) *)
   unfold lt in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: forall _ : @eq nat a (S b1), le (Init.Nat.mul a c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   rewrite (plus_comm d (b1 * d)).
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add (Init.Nat.mul a c) a) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_plus_trans.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul b1 d) *)
(* Goal: forall _ : @eq nat a (S b1), le (Init.Nat.mul a c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   apply IHb1.
(* Goal: le (Init.Nat.add b1 c) b1 *)
(* Goal: @eq nat (Init.Nat.add b1 c) (Init.Nat.add b1 c) *)
   apply le_S_n.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   rewrite H1.
(* Goal: le (Init.Nat.mul (S b1) c) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   replace (d + b1 * d) with (S b1 * d).
(* Goal: le (Init.Nat.mul (S b1) c) (Init.Nat.mul (S b1) d) *)
(* Goal: @eq nat (Init.Nat.mul (S b1) d) (Init.Nat.add d (Init.Nat.mul b1 d)) *)
(* Goal: le a (S b1) *)
   apply le_mult_l.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma lt_lt_mult : forall a b c d : nat, a < b -> c < d -> a * c < b * d.
Proof.
(* Goal: forall (a b c d : nat) (_ : lt a b) (_ : lt c d), lt (Init.Nat.mul a c) (Init.Nat.mul b d) *)
   unfold lt in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (S (Init.Nat.mul a c)) (Init.Nat.mul b d) *)
   apply le_trans with (S a * S c).
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: le (S (Init.Nat.mul a c)) (S (Init.Nat.add c (Init.Nat.mul a (S c)))) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_n_S.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add c (Init.Nat.mul a (S c))) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   rewrite <- (mult_n_Sm a c).
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add c (Init.Nat.add (Init.Nat.mul a c) a)) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   rewrite (plus_comm c (a * c + a)).
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add (Init.Nat.mul a c) a) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_plus_trans.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.add (Init.Nat.mul a c) a) *)
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_plus_trans.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply le_n.
(* Goal: le (Init.Nat.mul (S a) (S c)) (Init.Nat.mul b d) *)
   apply le_le_mult.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma lt_n_nm_m_gt_1 : forall a b : nat, a < a * b -> b > 1.
Proof.
(* Goal: forall (a b : Z) (_ : Z.le b a), Z.le Z0 (Z.sub a b) *)
   intros a b. case b.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   rewrite <- (mult_n_O a). intro. elim (lt_n_O a). assumption.
(* Goal: forall (n : nat) (_ : lt a (Init.Nat.mul a (S n))), gt (S n) (S O) *)
   intro b1. case b1.
(* Goal: forall _ : lt a (Init.Nat.mul a (S O)), gt (S O) (S O) *)
(* Goal: forall (n : nat) (_ : lt a (Init.Nat.mul a (S (S n)))), gt (S (S n)) (S O) *)
   rewrite <- (mult_n_Sm a 0).
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   rewrite <- (mult_n_O a). simpl in |- *. intro.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   elim (lt_irrefl a). assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. apply gt_n_S. apply gt_Sn_O.
Qed.

Lemma n0n1_or_gt : forall n : nat, n = 0 \/ n = 1 \/ n > 1.
Proof.
(* Goal: forall n : nat, or (@eq nat n O) (or (@eq nat n (S O)) (gt n (S O))) *)
   intro n. case n.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   left. reflexivity.
(* Goal: forall n : nat, or (@eq nat (S n) O) (or (@eq nat (S n) (S O)) (gt (S n) (S O))) *)
   intro n1. case n1.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   right. left. reflexivity.
(* Goal: forall n : nat, or (@eq nat (S (S n)) O) (or (@eq nat (S (S n)) (S O)) (gt (S (S n)) (S O))) *)
   intro n2.
(* Goal: forall _ : @eq Z Z0 Z0, or (@eq Z (Zneg p) Z0) (@eq Z Z0 Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zpos p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zpos p0) Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zneg p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zneg p0) Z0) *)
   right. right. apply gt_n_S. apply gt_Sn_O.
Qed.

Lemma lt_multpred_pp : forall p : nat, p > 1 -> pred p * pred p < p * p.
Proof.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: forall (q : nat) (_ : @eq nat (Init.Nat.mul p q) (S O)), and (@eq nat p (S O)) (@eq nat q (S O)) *)
   case p.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: lt (Init.Nat.mul (Init.Nat.pred O) (Init.Nat.pred O)) (Init.Nat.mul O O) *)
(* Goal: forall (n : nat) (_ : gt (S n) (S O)), lt (Init.Nat.mul (Init.Nat.pred (S n)) (Init.Nat.pred (S n))) (Init.Nat.mul (S n) (S n)) *)
   elim (lt_n_O 1).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S n) q) (S O)), and (@eq nat (S n) (S O)) (@eq nat q (S O)) *)
   intro p1.
(* Goal: forall (q : nat) (_ : @eq nat (Init.Nat.mul (S p1) q) (S O)), and (@eq nat (S p1) (S O)) (@eq nat q (S O)) *)
   case p1.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: lt (Init.Nat.mul (Init.Nat.pred (S O)) (Init.Nat.pred (S O))) (Init.Nat.mul (S O) (S O)) *)
(* Goal: forall (n : nat) (_ : gt (S (S n)) (S O)), lt (Init.Nat.mul (Init.Nat.pred (S (S n))) (Init.Nat.pred (S (S n)))) (Init.Nat.mul (S (S n)) (S (S n))) *)
   elim (lt_irrefl 1).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S (S n)) q) (S O)), and (@eq nat (S (S n)) (S O)) (@eq nat q (S O)) *)
   intro p2.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt (Init.Nat.mul (Init.Nat.pred (S (S p2))) (Init.Nat.pred (S (S p2)))) (Init.Nat.mul (S (S p2)) (S (S p2))) *)
   apply lt_lt_mult.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. apply lt_n_Sn.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. apply lt_n_Sn.
Qed.

Lemma le_diff0 : forall b a c : nat, a <= b -> a = b + c -> c = 0.
Proof.
(* Goal: forall (b : Z) (_ : @eq Z (Z.mul (Zneg p) b) Z0), or (@eq Z (Zneg p) Z0) (@eq Z b Z0) *)
   simple induction b.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intro.
(* Goal: forall (c : nat) (_ : le a O) (_ : @eq nat a c), @eq nat c O *)
(* Goal: forall (n : nat) (_ : forall (a c : nat) (_ : le a n) (_ : @eq nat a (Init.Nat.add n c)), @eq nat c O) (a c : nat) (_ : le a (S n)) (_ : @eq nat a (Init.Nat.add (S n) c)), @eq nat c O *)
   case a.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a b) *)
   rewrite H0.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   reflexivity.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: @eq nat c O *)
(* Goal: forall (n : nat) (_ : forall (a c : nat) (_ : le a n) (_ : @eq nat a (Init.Nat.add n c)), @eq nat c O) (a c : nat) (_ : le a (S n)) (_ : @eq nat a (Init.Nat.add (S n) c)), @eq nat c O *)
   elim (lt_n_O n).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : forall (a c : nat) (_ : le a n) (_ : @eq nat a (Init.Nat.add n c)), @eq nat c O) (a c : nat) (_ : le a (S n)) (_ : @eq nat a (Init.Nat.add (S n) c)), @eq nat c O *)
   intros b1 IH.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: False *)
   rewrite H0 in H.
(* Goal: @eq nat c O *)
   apply (IH (b1 + c) c).
(* Goal: le (Init.Nat.add b1 c) b1 *)
(* Goal: @eq nat (Init.Nat.add b1 c) (Init.Nat.add b1 c) *)
   apply le_S_n.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   reflexivity.
Qed.

Lemma simpl_lt_mult_l : forall a b c : nat, a * b < a * c -> b < c.
Proof.
(* Goal: forall (a b : Z) (_ : @eq Z (Z.mul a b) Z0), or (@eq Z a Z0) (@eq Z b Z0) *)
   simple induction a.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt b c *)
(* Goal: forall (n : nat) (_ : forall (b c : nat) (_ : lt (Init.Nat.mul n b) (Init.Nat.mul n c)), lt b c) (b c : nat) (_ : lt (Init.Nat.mul (S n) b) (Init.Nat.mul (S n) c)), lt b c *)
   elim (lt_irrefl 0).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : forall (b c : nat) (_ : lt O n) (_ : le (Init.Nat.mul n b) (Init.Nat.mul n c)), le b c) (b c : nat) (_ : lt O (S n)) (_ : le (Init.Nat.mul (S n) b) (Init.Nat.mul (S n) c)), le b c *)
   intros a1 IH.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le b c *)
   elim (le_or_lt b c).
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: lt b c *)
(* Goal: forall _ : lt c b, lt b c *)
   elim (le_lt_or_eq b c).
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt b c *)
(* Goal: le b c *)
(* Goal: forall _ : lt c b, lt b c *)
   rewrite H1 in H.
(* Goal: lt b c *)
(* Goal: le b c *)
(* Goal: forall _ : lt c b, lt b c *)
   elim (lt_irrefl (S a1 * c)).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt b c *)
   cut (S a1 * c <= S a1 * b).
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: lt b c *)
(* Goal: le (Init.Nat.mul (S a1) c) (Init.Nat.mul (S a1) b) *)
   elim (le_not_lt (S a1 * c) (S a1 * b)).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: le (Init.Nat.mul (S a1) c) (Init.Nat.mul (S a1) b) *)
   apply lt_le_weak.
(* Goal: lt (Init.Nat.mul (S a1) c) (Init.Nat.mul (S a1) b) *)
(* Goal: le (Init.Nat.mul (S a1) b) (Init.Nat.mul (S a1) c) *)
   apply lt_mult_l.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma simpl_le_mult_l : forall a b c : nat, 0 < a -> a * b <= a * c -> b <= c.
Proof.
(* Goal: forall (a b : Z) (_ : @eq Z (Z.mul a b) Z0), or (@eq Z a Z0) (@eq Z b Z0) *)
   simple induction a.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le b c *)
(* Goal: forall (n : nat) (_ : forall (b c : nat) (_ : lt O n) (_ : le (Init.Nat.mul n b) (Init.Nat.mul n c)), le b c) (b c : nat) (_ : lt O (S n)) (_ : le (Init.Nat.mul (S n) b) (Init.Nat.mul (S n) c)), le b c *)
   elim (lt_n_O 0).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (n : nat) (_ : forall (b c : nat) (_ : lt O n) (_ : le (Init.Nat.mul n b) (Init.Nat.mul n c)), le b c) (b c : nat) (_ : lt O (S n)) (_ : le (Init.Nat.mul (S n) b) (Init.Nat.mul (S n) c)), le b c *)
   intros a1 IH.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros.
(* Goal: le b c *)
   simpl in H0.
(* Goal: le b c *)
   elim (le_or_lt b c).
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: le b c *)
   elim (lt_not_le (S a1 * c) (S a1 * b)).
(* Goal: lt (Init.Nat.mul (S a1) c) (Init.Nat.mul (S a1) b) *)
(* Goal: le (Init.Nat.mul (S a1) b) (Init.Nat.mul (S a1) c) *)
   apply lt_mult_l.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma simpl_eq_mult_l : forall a b c : nat, 0 < a -> a * b = a * c -> b = c.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. apply le_antisym.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply simpl_le_mult_l with a. assumption. rewrite H0. apply le_n.
(* Goal: le (Init.Nat.mul a c) (Init.Nat.mul a c) *)
   apply simpl_le_mult_l with a. assumption. rewrite H0. apply le_n.
Qed.

Lemma mult_ppq_p0q1 : forall p q : nat, p = p * q -> p = 0 \/ q = 1.
Proof.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro p. case p. left. reflexivity.
(* Goal: forall _ : @eq Z Z0 Z0, or (@eq Z (Zneg p) Z0) (@eq Z Z0 Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zpos p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zpos p0) Z0) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.mul (Zneg p) (Zneg p0)) Z0), or (@eq Z (Zneg p) Z0) (@eq Z (Zneg p0) Z0) *)
   intro p1. right.
(* Goal: lt O (S p1) *)
(* Goal: @eq nat (Init.Nat.mul (S p1) q) (Init.Nat.mul (S p1) (S O)) *)
   apply simpl_eq_mult_l with (S p1). apply lt_O_Sn.
(* Goal: @eq nat (Init.Nat.mul (S p1) q) (Init.Nat.mul (S p1) (S O)) *)
   rewrite <- H.
(* Goal: forall _ : @eq nat (Init.Nat.mul (S (S p2)) (S O)) (S O), and (@eq nat (S (S p2)) (S O)) (@eq nat (S O) (S O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul (S (S p2)) (S (S n))) (S O)), and (@eq nat (S (S p2)) (S O)) (@eq nat (S (S n)) (S O)) *)
   rewrite <- mult_n_Sm. rewrite <- mult_n_O.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. reflexivity.
Qed.

Lemma mult_pq1_p1q1 : forall p q : nat, p * q = 1 -> p = 1 /\ q = 1.
Proof.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro p. case p. simpl in |- *. intros. discriminate H.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro p1. case p1. simpl in |- *.
(* Goal: @eq Z Z0 Z0 *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro q. rewrite <- plus_n_O. split. reflexivity. assumption.
(* Goal: forall (n q : nat) (_ : @eq nat (Init.Nat.mul (S (S n)) q) (S O)), and (@eq nat (S (S n)) (S O)) (@eq nat q (S O)) *)
   intro p2.
(* Goal: not (@eq Z x y) *)
   intro q. case q. rewrite <- mult_n_O. intro. discriminate H.
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul (S (S p2)) (S n)) (S O)), and (@eq nat (S (S p2)) (S O)) (@eq nat (S n) (S O)) *)
   intro q1. case q1.
(* Goal: forall _ : @eq nat (Init.Nat.mul (S (S p2)) (S O)) (S O), and (@eq nat (S (S p2)) (S O)) (@eq nat (S O) (S O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul (S (S p2)) (S (S n))) (S O)), and (@eq nat (S (S p2)) (S O)) (@eq nat (S (S n)) (S O)) *)
   rewrite <- mult_n_Sm.
(* Goal: forall _ : @eq nat (Init.Nat.add (Init.Nat.mul (S (S p2)) O) (S (S p2))) (S O), and (@eq nat (S (S p2)) (S O)) (@eq nat (S O) (S O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul (S (S p2)) (S (S n))) (S O)), and (@eq nat (S (S p2)) (S O)) (@eq nat (S (S n)) (S O)) *)
   rewrite <- mult_n_O.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intro. discriminate H.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intro q2. simpl in |- *. intro. discriminate H.
Qed.

Lemma Zmult_ab0a0b0 : forall a b : Z, (a * b)%Z = 0%Z -> a = 0%Z \/ b = 0%Z.
Proof.
(* Goal: forall (a b : Z) (_ : @eq Z (Z.mul a b) Z0), or (@eq Z a Z0) (@eq Z b Z0) *)
   simple induction a.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. left. reflexivity.
(* Goal: forall (b : Z) (_ : @eq Z (Z.mul (Zneg p) b) Z0), or (@eq Z (Zneg p) Z0) (@eq Z b Z0) *)
   intro p. simple induction b.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. right. reflexivity.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. discriminate H.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. discriminate H.
(* Goal: not (@eq Z x y) *)
   intro. simple induction b.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. right. reflexivity.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. discriminate H.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. intros. discriminate H.
Qed.

Lemma Zle_minus : forall a b : Z, (b <= a)%Z -> (0 <= a - b)%Z.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros a b. intros.
(* Goal: Z.le Z0 (Z.sub a b) *)
   apply Zplus_le_reg_l with b.
(* Goal: Z.le (Z.add b Z0) (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *. rewrite (Zplus_comm a).
(* Goal: Z.le (Z.add b Z0) (Z.add b (Z.add (Z.opp b) a)) *)
   rewrite (Zplus_assoc b (- b)). rewrite Zplus_opp_r.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   simpl in |- *. rewrite <- Zplus_0_r_reverse. assumption.
Qed.

Lemma Zopp_lt_gt_0 : forall x : Z, (x < 0)%Z -> (- x > 0)%Z.
Proof.
(* Goal: forall (x : Z) (_ : Z.lt x Z0), Z.gt (Z.opp x) Z0 *)
   simple induction x.
(* Goal: not (@eq Z x y) *)
   intro. unfold Zlt in H. simpl in H. discriminate H.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. unfold Zlt in H. simpl in H. discriminate H.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. simpl in |- *. unfold Zgt in |- *. simpl in |- *. reflexivity.
Qed.

Lemma Zlt_neq : forall x y : Z, (x < y)%Z -> x <> y.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. intro.
(* Goal: False *)
   rewrite H0 in H.
(* Goal: False *)
   elim (Zlt_irrefl y).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
Qed.

Lemma Zgt_neq : forall x y : Z, (x > y)%Z -> x <> y.
Proof.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. intro.
(* Goal: False *)
   rewrite H0 in H.
(* Goal: False *)
   elim (Zlt_irrefl y).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   apply Zgt_lt. assumption.
Qed.

Lemma S_inj : forall n m : nat, S n = S m -> n = m.
(* Goal: forall (n m : nat) (_ : @eq nat (S n) (S m)), @eq nat n m *)
  intros n m H; injection H; trivial.
Qed.

Lemma Zlt_mult_l :
 forall p q r : Z, (0 < r)%Z -> (p < q)%Z -> (r * p < r * q)%Z.
Proof.
(* Goal: forall (p q r : Z) (_ : Z.lt Z0 r) (_ : Z.le p q), Z.le (Z.mul r p) (Z.mul r q) *)
   simple induction r.
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. elim (Zlt_irrefl 0). assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. unfold Zlt in |- *.
(* Goal: not (@eq comparison (Z.compare (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q)) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   rewrite (Zcompare_mult_compat p0 p q).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. unfold Zlt in H. simpl in H. discriminate H.
Qed.

Lemma Zle_mult_l :
 forall p q r : Z, (0 < r)%Z -> (p <= q)%Z -> (r * p <= r * q)%Z.
Proof.
(* Goal: forall (p q r : Z) (_ : Z.lt Z0 r) (_ : Z.le p q), Z.le (Z.mul r p) (Z.mul r q) *)
   simple induction r.
(* Goal: Z.le (Z.mul Z0 p) (Z.mul Z0 q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zpos p0)) (_ : Z.le p q), Z.le (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. simpl in |- *. apply Zeq_le. reflexivity.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. unfold Zle in |- *.
(* Goal: not (@eq comparison (Z.compare (Z.mul (Zpos p0) p) (Z.mul (Zpos p0) q)) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   rewrite (Zcompare_mult_compat p0 p q).
(* Goal: not (@eq comparison (Z.compare p q) Gt) *)
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   assumption.
(* Goal: forall (p0 : positive) (_ : Z.lt Z0 (Zneg p0)) (_ : Z.le p q), Z.le (Z.mul (Zneg p0) p) (Z.mul (Zneg p0) q) *)
   intros. unfold Zlt in H. simpl in H. discriminate H.
Qed.
