(****************************************************************************
                                                                             
          IEEE754  :  Faux                                                   
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Auxillary properties about natural numbers, relative numbers and reals *)
Require Export Min.
Require Export Arith.
Require Export Reals.
Require Export Zpower.
Require Export ZArith.
Require Export Zcomplements.
Require Export sTactic.
Hint Resolve R1_neq_R0: real.
(*Missing rule for nat *)
 
Theorem minus_minus : forall a b : nat, a <= b -> b - (b - a) = a.
(* Goal: forall (a b : nat) (_ : le a b), @eq nat (Init.Nat.sub b (Init.Nat.sub b a)) a *)
intros a b H'.
(* Goal: @eq nat (Init.Nat.sub b (Init.Nat.sub b a)) a *)
apply sym_equal.
(* Goal: @eq nat a (Init.Nat.sub b (Init.Nat.sub b a)) *)
apply plus_minus; auto.
(* Goal: @eq nat b (Init.Nat.add (Init.Nat.sub b a) a) *)
rewrite plus_comm; apply le_plus_minus; auto.
Qed.
 
Theorem lte_comp_mult :
 forall p q r t : nat, p <= q -> r <= t -> p * r <= q * t.
(* Goal: forall (p q r t : nat) (_ : le p q) (_ : le r t), le (Init.Nat.mul p r) (Init.Nat.mul q t) *)
intros p q r t H'; elim H'; simpl in |- *; auto with arith.
(* Goal: forall (m : nat) (_ : le p m) (_ : forall _ : le r t, le (Init.Nat.mul p r) (Init.Nat.mul m t)) (_ : le r t), le (Init.Nat.mul p r) (Init.Nat.add t (Init.Nat.mul m t)) *)
elim p; simpl in |- *; auto with arith.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : le n m) (_ : forall _ : le r t, le (Init.Nat.mul n r) (Init.Nat.mul m t)) (_ : le r t), le (Init.Nat.mul n r) (Init.Nat.add t (Init.Nat.mul m t))) (m : nat) (_ : le (S n) m) (_ : forall _ : le r t, le (Init.Nat.add r (Init.Nat.mul n r)) (Init.Nat.mul m t)) (_ : le r t), le (Init.Nat.add r (Init.Nat.mul n r)) (Init.Nat.add t (Init.Nat.mul m t)) *)
intros n H m H0 H1 H2; apply plus_le_compat; auto with arith.
(* Goal: le (Init.Nat.mul n r) (Init.Nat.mul m t) *)
apply le_trans with (m := r + n * r); auto with arith.
Qed.
Hint Resolve lte_comp_mult: arith.
 
Theorem le_refl_eq : forall n m : nat, n = m -> n <= m.
(* Goal: forall (n m : nat) (_ : @eq nat n m), le n m *)
intros n m H'; rewrite H'; auto.
Qed.
 
Theorem lt_le_pred : forall n m : nat, n < m -> n <= pred m.
(* Goal: forall (n m : nat) (_ : lt n m), le n (Init.Nat.pred m) *)
intros n m H'; inversion H'; simpl in |- *; auto.
(* Goal: le n m0 *)
apply le_trans with (S n); auto.
Qed.
 
Theorem lt_comp_mult_l : forall p q r : nat, 0 < p -> q < r -> p * q < p * r.
(* Goal: forall (p q r : nat) (_ : lt O p) (_ : lt q r), lt (Init.Nat.mul p q) (Init.Nat.mul p r) *)
intros p; elim p; simpl in |- *.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
auto with arith.
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n0; case n0.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
simpl in |- *; auto with arith.
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.mul (S n) q) (Init.Nat.mul (S n) r)) (q r : nat) (_ : lt O (S (S n))) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul (S n) q)) (Init.Nat.add r (Init.Nat.mul (S n) r)) *)
intros n1 H' q r H'0 H'1.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply lt_trans with (m := q + S n1 * r); auto with arith.
Qed.
Hint Resolve lt_comp_mult_l: arith.
 
Theorem lt_comp_mult_r : forall p q r : nat, 0 < p -> q < r -> q * p < r * p.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros; repeat rewrite (fun x : nat => mult_comm x p); auto with arith.
Qed.
Hint Resolve lt_comp_mult_r: arith.
 
Theorem lt_comp_mult : forall p q r s : nat, p < q -> r < s -> p * r < q * s.
(* Goal: forall (p q r s : nat) (_ : lt p q) (_ : lt r s), lt (Init.Nat.mul p r) (Init.Nat.mul q s) *)
intros p q r s; case q.
(* Goal: forall (_ : lt p O) (_ : lt r s), lt (Init.Nat.mul p r) (Init.Nat.mul O s) *)
(* Goal: forall (n : nat) (_ : lt p (S n)) (_ : lt r s), lt (Init.Nat.mul p r) (Init.Nat.mul (S n) s) *)
intros H'; inversion H'.
(* Goal: forall (n : nat) (_ : lt p (S n)) (_ : lt r s), lt (Init.Nat.mul p r) (Init.Nat.mul (S n) s) *)
intros q'; case p.
intros H' H'0; simpl in |- *; apply le_lt_trans with (m := r);
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
 auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros p' H' H'0; apply le_lt_trans with (m := S q' * r); auto with arith.
Qed.
Hint Resolve lt_comp_mult: arith.
 
Theorem mult_eq_inv : forall n m p : nat, 0 < n -> n * m = n * p -> m = p.
(* Goal: forall (n m p : nat) (_ : lt O n) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul n p)), @eq nat m p *)
intros n m p H' H'0.
(* Goal: @eq nat m p *)
apply le_antisym; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
case (le_or_lt m p); intros H'1; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
absurd (n * p < n * m); auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite H'0; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
case (le_or_lt p m); intros H'1; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
absurd (n * m < n * p); auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite H'0; auto with arith.
Qed.
 
Definition natEq : forall n m : nat, {n = m} + {n <> m}.
(* Goal: forall n m : nat, sumbool (@eq nat n m) (not (@eq nat n m)) *)
intros n; elim n.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros m; case m; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n0 H' m; case m; auto with arith.
Defined.
 
Theorem notEqLt : forall n : nat, 0 < n -> n <> 0.
(* Goal: forall (n : nat) (_ : lt O n), not (@eq nat n O) *)
intros n H'; Contradict H'; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite H'; auto with arith.
Qed.
Hint Resolve notEqLt: arith.
 
Theorem lt_next : forall n m : nat, n < m -> m = S n \/ S n < m.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n m H'; elim H'; auto with arith.
Qed.
 
Theorem le_next : forall n m : nat, n <= m -> m = n \/ S n <= m.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n m H'; case (le_lt_or_eq _ _ H'); auto with arith.
Qed.
 
Theorem min_or :
 forall n m : nat, min n m = n /\ n <= m \/ min n m = m /\ m < n.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n; elim n; simpl in |- *; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n' Rec m; case m; simpl in |- *; auto with arith.
intros m'; elim (Rec m'); intros H'0; case H'0; clear H'0; intros H'0 H'1;
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
 rewrite H'0; auto with arith.
Qed.
 
Theorem minus_inv_lt_aux : forall n m : nat, n - m = 0 -> n - S m = 0.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n; elim n; simpl in |- *; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n0 H' m; case m; auto with arith.
(* Goal: forall _ : @eq nat (S n0) O, @eq nat (Init.Nat.sub n0 O) O *)
intros H'0; discriminate.
Qed.
 
Theorem minus_inv_lt : forall n m : nat, m <= n -> m - n = 0.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n m H'; elim H'; simpl in |- *; auto with arith.
(* Goal: forall (m0 : nat) (_ : le m m0) (_ : @eq nat (Init.Nat.sub m m0) O), @eq nat (Init.Nat.sub m (S m0)) O *)
intros m0 H'0 H'1; apply minus_inv_lt_aux; auto.
Qed.
 
Theorem minus_le : forall m n p q : nat, m <= n -> p <= q -> m - q <= n - p.
(* Goal: forall (m n p q : nat) (_ : le m n) (_ : le p q), le (Init.Nat.sub m q) (Init.Nat.sub n p) *)
intros m n p q H' H'0.
(* Goal: le (Init.Nat.sub m q) (Init.Nat.sub n p) *)
case (le_or_lt m q); intros H'1.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite minus_inv_lt with (1 := H'1); auto with arith.
(* Goal: le (Init.Nat.sub m q) (Init.Nat.sub n p) *)
apply (fun p n m : nat => plus_le_reg_l n m p) with (p := q).
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite le_plus_minus_r; auto with arith.
(* Goal: le m (Init.Nat.add q (Init.Nat.sub n p)) *)
rewrite (le_plus_minus p q); auto.
(* Goal: le m (Init.Nat.add (Init.Nat.add p (Init.Nat.sub q p)) (Init.Nat.sub n p)) *)
rewrite (plus_comm p).
(* Goal: le m (Init.Nat.add (Nat.add (Init.Nat.sub q p) p) (Init.Nat.sub n p)) *)
rewrite plus_assoc_reverse.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite le_plus_minus_r; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply le_trans with (1 := H'); auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply le_trans with (1 := H'0); auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply le_trans with (2 := H'); auto with arith.
Qed.
 
Theorem lt_minus_inv : forall n m p : nat, n <= p -> m < n -> p - n < p - m.
(* Goal: forall (n m p : nat) (_ : le n p) (_ : lt m n), lt (Init.Nat.sub p n) (Init.Nat.sub p m) *)
intros n m p H'; generalize m; clear m; elim H'.
(* Goal: forall (m : nat) (_ : lt m n), lt (Init.Nat.sub n n) (Init.Nat.sub n m) *)
(* Goal: forall (m : nat) (_ : le n m) (_ : forall (m0 : nat) (_ : lt m0 n), lt (Init.Nat.sub m n) (Init.Nat.sub m m0)) (m0 : nat) (_ : lt m0 n), lt (Init.Nat.sub (S m) n) (Init.Nat.sub (S m) m0) *)
intros m H'0; rewrite <- minus_n_n; elim H'0.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
rewrite <- minus_Sn_m; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros m0 H'1 H'2; rewrite <- minus_Sn_m; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros m H'0 H'1 m0 H'2; repeat rewrite <- minus_Sn_m; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply le_trans with n; auto with arith.
Qed.
 
Theorem lt_mult_anti_compatibility :
 forall n n1 n2 : nat, 0 < n -> n * n1 < n * n2 -> n1 < n2.
(* Goal: forall (n n1 n2 : nat) (_ : lt O n) (_ : lt (Init.Nat.mul n n1) (Init.Nat.mul n n2)), lt n1 n2 *)
intros n n1 n2 H' H'0; case (le_or_lt n2 n1); auto.
(* Goal: forall _ : lt n2 n1, le n1 n2 *)
intros H'1; Contradict H'0; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply le_not_lt; auto with arith.
Qed.
 
Theorem le_mult_anti_compatibility :
 forall n n1 n2 : nat, 0 < n -> n * n1 <= n * n2 -> n1 <= n2.
(* Goal: forall (n n1 n2 : nat) (_ : lt O n) (_ : le (Init.Nat.mul n n1) (Init.Nat.mul n n2)), le n1 n2 *)
intros n n1 n2 H' H'0; case (le_or_lt n1 n2); auto.
(* Goal: forall _ : lt n2 n1, le n1 n2 *)
intros H'1; Contradict H'0; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
apply lt_not_le; auto with arith.
Qed.
 
Theorem min_n_0 : forall n : nat, min n 0 = 0.
(* Goal: forall n : nat, @eq nat (Nat.min n O) O *)
intros n; case n; simpl in |- *; auto.
Qed.
(*Simplification rules missing in R *)
Hint Resolve Rabs_pos: real.
 
Theorem Rlt_Rminus_ZERO : forall r1 r2 : R, (r2 < r1)%R -> (0 < r1 - r2)%R.
intros r1 r2 H; replace 0%R with (r1 - r1)%R; unfold Rminus in |- *;
 auto with real.
Qed.
Hint Resolve Rlt_Rminus_ZERO: real.
 
Theorem Rabsolu_left1 : forall a : R, (a <= 0)%R -> Rabs a = (- a)%R.
(* Goal: forall (a : R) (_ : Rle a (IZR Z0)), @eq R (Rabs a) (Ropp a) *)
intros a H; case H; intros H1.
(* Goal: @eq R (Rabs a) (Ropp a) *)
(* Goal: @eq R (Rabs a) (Ropp a) *)
apply Rabs_left; auto.
(* Goal: @eq R (Rabs a) (Ropp a) *)
rewrite H1; simpl in |- *; rewrite Rabs_right; auto with real.
Qed.
 
Theorem RmaxLess1 : forall r1 r2 : R, (r1 <= Rmax r1 r2)%R.
(* Goal: forall r1 r2 : R, Rle r1 (Rmax r1 r2) *)
intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real.
Qed.
 
Theorem RmaxLess2 : forall r1 r2 : R, (r2 <= Rmax r1 r2)%R.
intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real;
 intros; apply Ropp_le_cancel; auto with real.
Qed.
 
Theorem RmaxSym : forall p q : R, Rmax p q = Rmax q p.
(* Goal: forall p q : R, @eq R (Rmax p q) (Rmax q p) *)
intros p q; unfold Rmax in |- *.
case (Rle_dec p q); case (Rle_dec q p); auto; intros H1 H2; apply Rle_antisym;
 auto.
(* Goal: Rle p q *)
(* Goal: Rle q p *)
case (Rle_or_lt p q); auto; intros H'0; Contradict H1; apply Rlt_le; auto.
(* Goal: Rle q p *)
case (Rle_or_lt q p); auto; intros H'0; Contradict H2; apply Rlt_le; auto.
Qed.
 
Theorem RmaxAbs :
 forall p q r : R,
 (p <= q)%R -> (q <= r)%R -> (Rabs q <= Rmax (Rabs p) (Rabs r))%R.
(* Goal: forall (p q r : R) (_ : Rle p q) (_ : Rle q r), Rle (Rabs q) (Rmax (Rabs p) (Rabs r)) *)
intros p q r H' H'0; case (Rle_or_lt 0 p); intros H'1.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle q (Rmax p r) *)
(* Goal: Rge r (IZR Z0) *)
(* Goal: Rge q (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Rabs p) (Rabs r)) *)
apply Rle_trans with r; auto with real.
(* Goal: Rle r (Rmax (Ropp p) r) *)
(* Goal: Rge r (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
apply RmaxLess2; auto.
apply Rge_trans with p; auto with real; apply Rge_trans with q;
 auto with real.
(* Goal: Rge q (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Rabs p) (Rabs r)) *)
apply Rge_trans with p; auto with real.
(* Goal: Rle (Rabs q) (Rmax (Rabs p) (Rabs r)) *)
rewrite (Rabs_left p); auto.
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
case (Rle_or_lt 0 q); intros H'2.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle q (Rmax (Ropp p) r) *)
(* Goal: Rge r (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
apply Rle_trans with r; auto.
(* Goal: Rle r (Rmax (Ropp p) r) *)
(* Goal: Rge r (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
apply RmaxLess2; auto.
(* Goal: Rge r (IZR Z0) *)
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
apply Rge_trans with q; auto with real.
(* Goal: Rle (Rabs q) (Rmax (Ropp p) (Rabs r)) *)
rewrite (Rabs_left q); auto.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
case (Rle_or_lt 0 r); intros H'3.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Ropp r)) *)
apply Rle_trans with (- p)%R; auto with real.
(* Goal: Rle (Ropp p) (Rmax (Ropp p) (Ropp r)) *)
apply RmaxLess1; auto.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Rabs r)) *)
rewrite (Rabs_left r); auto.
(* Goal: Rle (Ropp q) (Rmax (Ropp p) (Ropp r)) *)
apply Rle_trans with (- p)%R; auto with real.
(* Goal: Rle (Ropp p) (Rmax (Ropp p) (Ropp r)) *)
apply RmaxLess1; auto.
Qed.
 
Theorem Rabsolu_Zabs : forall z : Z, Rabs (IZR z) = IZR (Zabs z).
(* Goal: forall z : Z, @eq R (Rabs (IZR z)) (IZR (Z.abs z)) *)
intros z; case z; simpl in |- *; auto with real.
(* Goal: @eq R (Rabs (IZR Z0)) (IZR Z0) *)
(* Goal: forall p : positive, @eq R (Rabs (IZR (Zpos p))) (IZR (Zpos p)) *)
(* Goal: forall p : positive, @eq R (Rabs (IZR (Zneg p))) (IZR (Zpos p)) *)
apply Rabs_right; auto with real.
(* Goal: forall p : positive, @eq R (Rabs (IZR (Zpos p))) (IZR (Zpos p)) *)
(* Goal: forall p : positive, @eq R (Rabs (IZR (Zneg p))) (IZR (Zpos p)) *)
intros p0; apply Rabs_right; auto with real zarith.
(* Goal: forall p : positive, @eq R (Rabs (IZR (Zneg p))) (IZR (Zpos p)) *)
intros p0; unfold IZR; rewrite <- INR_IPR; rewrite Rabs_Ropp.
(* Goal: @eq R (Rabs (INR (Pos.to_nat p0))) (INR (Pos.to_nat p0)) *)
apply Rabs_right; auto with real zarith.
Qed.
 
Theorem RmaxRmult :
 forall p q r : R, (0 <= r)%R -> Rmax (r * p) (r * q) = (r * Rmax p q)%R.
(* Goal: forall (p q r : R) (_ : Rle (IZR Z0) r), @eq R (Rmax (Rmult r p) (Rmult r q)) (Rmult r (Rmax p q)) *)
intros p q r H; unfold Rmax in |- *.
(* Goal: @eq R (if Rle_dec (Rmult r p) (Rmult r q) then Rmult r q else Rmult r p) (Rmult r (if Rle_dec p q then q else p)) *)
case (Rle_dec p q); case (Rle_dec (r * p) (r * q)); auto; intros H1 H2; auto.
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
case H; intros E1.
(* Goal: @eq R (Rmult r p) (Rmult r q) *)
(* Goal: @eq R (Rmult r p) (Rmult r q) *)
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
case H1; auto with real.
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
rewrite <- E1; repeat rewrite Rmult_0_l; auto.
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
case H; intros E1.
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
case H2; auto with real.
(* Goal: Rle p q *)
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
apply Rmult_le_reg_l with (r := r); auto.
(* Goal: @eq R (Rmult r q) (Rmult r p) *)
rewrite <- E1; repeat rewrite Rmult_0_l; auto.
Qed.
 
Theorem Rle_R0_Ropp : forall p : R, (p <= 0)%R -> (0 <= - p)%R.
(* Goal: forall (p : R) (_ : Rlt p (IZR Z0)), Rlt (IZR Z0) (Ropp p) *)
intros p H; rewrite <- Ropp_0; auto with real.
Qed.
 
Theorem Rlt_R0_Ropp : forall p : R, (p < 0)%R -> (0 < - p)%R.
(* Goal: forall (p : R) (_ : Rlt p (IZR Z0)), Rlt (IZR Z0) (Ropp p) *)
intros p H; rewrite <- Ropp_0; auto with real.
Qed.
Hint Resolve Rle_R0_Ropp Rlt_R0_Ropp: real.
(* Properties of Z *)
 
Theorem convert_not_O : forall p : positive, nat_of_P p <> 0.
(* Goal: forall p : positive, not (@eq nat (Pos.to_nat p) O) *)
intros p; elim p.
(* Goal: forall (p : positive) (_ : not (@eq nat (Pos.to_nat p) O)), not (@eq nat (Pos.to_nat (xO p)) O) *)
(* Goal: not (@eq nat (Pos.to_nat xH) O) *)
intros p0 H'; unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6.
(* Goal: not (@eq nat (S (Init.Nat.add (Pos.to_nat p0) (Pos.to_nat p0))) O) *)
(* Goal: forall (p : positive) (_ : not (@eq nat (Pos.to_nat p) O)), not (@eq nat (Pos.to_nat (xO p)) O) *)
(* Goal: not (@eq nat (Pos.to_nat xH) O) *)
generalize H'; case (nat_of_P p0); auto.
(* Goal: forall (p : positive) (_ : not (@eq nat (Pos.to_nat p) O)), not (@eq nat (Pos.to_nat (xO p)) O) *)
(* Goal: not (@eq nat (Pos.to_nat xH) O) *)
intros p0 H'; unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6.
(* Goal: not (@eq nat (Init.Nat.add (Pos.to_nat p0) (Pos.to_nat p0)) O) *)
(* Goal: not (@eq nat (Pos.to_nat xH) O) *)
generalize H'; case (nat_of_P p0); simpl in |- *; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
unfold nat_of_P in |- *; simpl in |- *; auto with arith.
Qed.
Hint Resolve convert_not_O: zarith arith.
Hint Resolve Zlt_le_weak Zle_not_gt Zgt_irrefl Zlt_irrefl Zle_not_lt
  Zlt_not_le Zlt_asym inj_lt inj_le: zarith.
 
Theorem inj_abs :
 forall x : Z, (0 <= x)%Z -> Z_of_nat (Zabs_nat x) = x.
(* Goal: forall (x : Z) (_ : Z.le Z0 x), @eq Z (Z.of_nat (Z.abs_nat x)) x *)
intros x; elim x; auto.
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zpos p)), @eq Z (Z.of_nat (Z.abs_nat (Zpos p))) (Zpos p) *)
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zneg p)), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
unfold Zabs_nat in |- *.
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zpos p)), @eq Z (Z.of_nat (Pos.to_nat p)) (Zpos p) *)
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zneg p)), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
intros p.
pattern p at 1 3 in |- *;
 rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id p).
generalize (convert_not_O p); case (nat_of_P p); simpl in |- *;
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
 auto with arith.
(* Goal: forall _ : not (@eq comparison Gt Gt), @eq Z z1 z2 *)
intros H'; case H'; auto.
(* Goal: forall (n : nat) (_ : not (@eq nat (S n) O)) (_ : Z.le Z0 (Zpos (Pos.pred (Pos.succ (Pos.of_succ_nat n))))), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos (Pos.pred (Pos.succ (Pos.of_succ_nat n)))) *)
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zneg p)), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
intros n H' H'0; rewrite Ppred_succ; auto.
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zneg p)), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
intros p H'; Contradict H'; auto.
Qed.
 
Theorem inject_nat_convert :
 forall (p : Z) (q : positive),
 p = Zpos q -> Z_of_nat (nat_of_P q) = p.
(* Goal: forall (p : Z) (q : positive) (_ : @eq Z p (Zpos q)), @eq Z (Z.of_nat (Pos.to_nat q)) p *)
intros p q H'; rewrite H'.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat q)) (Zpos q) *)
CaseEq (nat_of_P q); simpl in |- *.
elim q; unfold nat_of_P in |- *; simpl in |- *; intros;
 try discriminate.
(* Goal: @eq Z Z0 (Zpos (xO p0)) *)
(* Goal: forall (n : nat) (_ : @eq nat (Pos.to_nat q) (S n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
absurd (0%Z = Zpos p0); auto.
(* Goal: not (@eq Z Z0 (Zpos p0)) *)
(* Goal: @eq Z Z0 (Zpos p0) *)
(* Goal: forall (n : nat) (_ : @eq nat (Pos.to_nat q) (S n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
red in |- *; intros H'0; try discriminate.
(* Goal: @eq Z Z0 (Zpos p0) *)
(* Goal: forall (n : nat) (_ : @eq nat (Pos.to_nat q) (S n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
apply H; auto.
(* Goal: @eq nat (Pos.iter_op nat Init.Nat.add p0 (S O)) O *)
(* Goal: forall (n : nat) (_ : @eq nat (Pos.to_nat q) (S n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
change (nat_of_P p0 = 0) in |- *.
generalize H0; rewrite ZL6; case (nat_of_P p0); simpl in |- *;
 auto; intros; try discriminate.
(* Goal: forall (n : nat) (_ : @eq nat (Pos.to_nat q) (S n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
intros n; rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
(* Goal: forall _ : @eq nat (Pos.to_nat q) (Pos.to_nat (Pos.of_succ_nat n)), @eq Z (Zpos (Pos.of_succ_nat n)) (Zpos q) *)
intros H'0; apply f_equal with (f := Zpos).
(* Goal: @eq positive (Pos.of_succ_nat n) q *)
apply nat_of_P_inj; auto.
Qed.
Hint Resolve inj_le inj_lt: zarith.
 
Theorem ZleLe : forall x y : nat, (Z_of_nat x <= Z_of_nat y)%Z -> x <= y.
(* Goal: forall (x y : Z) (_ : Z.le x y), Rle (IZR x) (IZR y) *)
intros x y H'.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
case (le_or_lt x y); auto with arith.
(* Goal: forall _ : lt y x, le x y *)
intros H'0; Contradict H'; auto with zarith.
Qed.
 
Theorem inject_nat_eq : forall x y : nat, Z_of_nat x = Z_of_nat y -> x = y.
(* Goal: forall (x y : nat) (_ : @eq Z (Z.of_nat x) (Z.of_nat y)), @eq nat x y *)
intros x y H'; apply le_antisym.
(* Goal: le y x *)
apply ZleLe; auto.
(* Goal: Z.le (Z.of_nat y) (Z.of_nat x) *)
idtac; rewrite H'; auto with zarith.
(* Goal: le y x *)
apply ZleLe; auto.
(* Goal: Z.le (Z.of_nat y) (Z.of_nat x) *)
idtac; rewrite H'; auto with zarith.
Qed.
 
Theorem Zcompare_EGAL :
 forall p q : Z, (p ?= q)%Z = Datatypes.Eq -> p = q.
intros p q; case p; case q; simpl in |- *; auto with arith;
 try (intros; discriminate); intros q1 p1.
(* Goal: forall _ : @eq comparison (Pos.compare p1 q1) Eq, @eq Z (Zpos p1) (Zpos q1) *)
(* Goal: forall _ : @eq comparison (CompOpp (Pos.compare p1 q1)) Eq, @eq Z (Zneg p1) (Zneg q1) *)
intros H1; rewrite (Pcompare_Eq_eq p1 q1); auto.
(* Goal: forall _ : @eq comparison (CompOpp (Pos.compare p1 q1)) Eq, @eq Z (Zneg p1) (Zneg q1) *)
unfold Pos.compare.
generalize (Pcompare_Eq_eq p1 q1);
 case (Pcompare p1 q1 Datatypes.Eq); simpl in |- *; 
 intros H H1; try discriminate; rewrite H; auto.
Qed.
 
Theorem Zlt_Zopp : forall x y : Z, (x < y)%Z -> (- y < - x)%Z.
intros x y; case x; case y; simpl in |- *; auto with zarith; intros p p0;
 unfold Zlt in |- *; simpl in |- *; unfold Pos.compare; rewrite <- ZC4;
 auto.
Qed.
Hint Resolve Zlt_Zopp: zarith.
 
Theorem Zle_Zopp : forall x y : Z, (x <= y)%Z -> (- y <= - x)%Z.
(* Goal: forall (x y : Z) (_ : Z.le x y), Z.le (Z.opp y) (Z.opp x) *)
intros x y H'; case (Zle_lt_or_eq _ _ H'); auto with zarith.
Qed.
Hint Resolve Zle_Zopp: zarith.
 
Theorem absolu_INR : forall n : nat, Zabs_nat (Z_of_nat n) = n.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n; case n; simpl in |- *; auto with arith.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n0; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith.
Qed.
 
Theorem absolu_Zopp : forall p : Z, Zabs_nat (- p) = Zabs_nat p.
(* Goal: forall (p : Z) (_ : @eq R (IZR p) (IZR Z0)), @eq Z p Z0 *)
intros p; case p; simpl in |- *; auto.
Qed.
 
Theorem Zabs_absolu : forall z : Z, Zabs z = Z_of_nat (Zabs_nat z).
intros z; case z; simpl in |- *; auto; intros p; apply sym_equal;
 apply inject_nat_convert; auto.
Qed.
 
Theorem absolu_comp_mult :
 forall p q : Z, Zabs_nat (p * q) = Zabs_nat p * Zabs_nat q.
intros p q; case p; case q; simpl in |- *; auto; intros p0 p1;
 apply
  ((fun (x y : positive) (_ : positive -> positive) =>
    nat_of_P_mult_morphism x y) p1 p0 (fun x => x)).
Qed.
 
Theorem Zmin_sym : forall m n : Z, Zmin n m = Zmin m n.
(* Goal: forall m n : Z, @eq Z (Z.min n m) (Z.min m n) *)
intros m n; unfold Zmin in |- *.
(* Goal: forall _ : @eq comparison (CompOpp (Pos.compare p1 q1)) Eq, @eq Z (Zneg p1) (Zneg q1) *)
case n; case m; simpl in |- *; auto; unfold Pos.compare.
(* Goal: forall p p0 : positive, @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (Pos.compare_cont Eq p p0) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
intros p p0; rewrite (ZC4 p p0).
(* Goal: @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (CompOpp (Pos.compare_cont Eq p0 p)) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
generalize (Pcompare_Eq_eq p0 p).
(* Goal: forall _ : forall _ : @eq comparison (Pos.compare_cont Eq p0 p) Eq, @eq positive p0 p, @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (CompOpp (Pos.compare_cont Eq p0 p)) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
case (Pcompare p0 p Datatypes.Eq); simpl in |- *; auto.
(* Goal: forall _ : forall _ : @eq comparison Eq Eq, @eq positive p0 p, @eq Z (Zneg p0) (Zneg p) *)
intros H'; rewrite H'; auto.
(* Goal: forall p p0 : positive, @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (Pos.compare_cont Eq p p0) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
intros p p0; rewrite (ZC4 p p0).
(* Goal: @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (CompOpp (Pos.compare_cont Eq p0 p)) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
generalize (Pcompare_Eq_eq p0 p).
(* Goal: forall _ : forall _ : @eq comparison (Pos.compare_cont Eq p0 p) Eq, @eq positive p0 p, @eq Z match CompOpp (Pos.compare_cont Eq p0 p) with | Eq => Zneg p0 | Lt => Zneg p0 | Gt => Zneg p end match CompOpp (CompOpp (Pos.compare_cont Eq p0 p)) with | Eq => Zneg p | Lt => Zneg p | Gt => Zneg p0 end *)
case (Pcompare p0 p Datatypes.Eq); simpl in |- *; auto.
(* Goal: forall _ : forall _ : @eq comparison Eq Eq, @eq positive p0 p, @eq Z (Zneg p0) (Zneg p) *)
intros H'; rewrite H'; auto.
Qed.
 
Theorem Zpower_nat_O : forall z : Z, Zpower_nat z 0 = Z_of_nat 1.
(* Goal: forall z : Z, @eq Z (Zpower_nat z O) (Z.of_nat (S O)) *)
intros z; unfold Zpower_nat in |- *; simpl in |- *; auto.
Qed.
 
Theorem Zpower_nat_1 : forall z : Z, Zpower_nat z 1 = z.
(* Goal: forall z : Z, @eq Z (Zpower_nat z (S O)) z *)
intros z; unfold Zpower_nat in |- *; simpl in |- *; rewrite Zmult_1_r; auto.
Qed.
 
Theorem Zmin_le1 : forall z1 z2 : Z, (z1 <= z2)%Z -> Zmin z1 z2 = z1.
intros z1 z2; unfold Zle, Zmin in |- *; case (z1 ?= z2)%Z; auto; intros H;
 Contradict H; auto.
Qed.
 
Theorem Zmin_le2 : forall z1 z2 : Z, (z2 <= z1)%Z -> Zmin z1 z2 = z2.
(* Goal: forall (z1 z2 : Z) (_ : Z.le z2 z1), @eq Z (Z.min z1 z2) z2 *)
intros z1 z2 H; rewrite Zmin_sym; apply Zmin_le1; auto.
Qed.
 
Theorem Zmin_Zle :
 forall z1 z2 z3 : Z,
 (z1 <= z2)%Z -> (z1 <= z3)%Z -> (z1 <= Zmin z2 z3)%Z.
(* Goal: forall (z1 z2 z3 : Z) (_ : Z.le z1 z2) (_ : Z.le z1 z3), Z.le z1 (Z.min z2 z3) *)
intros z1 z2 z3 H' H'0; unfold Zmin in |- *.
(* Goal: Z.le z1 match Z.compare z2 z3 with | Eq => z2 | Lt => z2 | Gt => z3 end *)
case (z2 ?= z3)%Z; auto.
Qed.
 
Theorem Zminus_n_predm :
 forall n m : Z, Zsucc (n - m) = (n - Zpred m)%Z.
(* Goal: forall n m : Z, @eq Z (Z.succ (Z.sub n m)) (Z.sub n (Z.pred m)) *)
intros n m.
(* Goal: @eq Z (Z.succ (Z.sub n m)) (Z.sub n (Z.pred m)) *)
unfold Zpred in |- *; unfold Zsucc in |- *; ring.
Qed.
 
Theorem Zopp_Zpred_Zs : forall z : Z, (- Zpred z)%Z = Zsucc (- z).
(* Goal: forall z : Z, @eq Z (Z.pred (Z.opp z)) (Z.opp (Z.succ z)) *)
intros z; unfold Zpred, Zsucc in |- *; ring.
Qed.
 
Theorem Zle_mult_gen :
 forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * y)%Z.
(* Goal: forall (x y : Z) (_ : Z.le Z0 x) (_ : Z.le Z0 y), Z.le Z0 (Z.mul x y) *)
intros x y H' H'0; case (Zle_lt_or_eq _ _ H').
intros H'1; rewrite Zmult_comm; apply Zmult_gt_0_le_0_compat; auto;
(* Goal: Z.gt z Z0 *)
(* Goal: Z.le (Z.mul x z) (Z.mul y z) *)
 apply Zlt_gt; auto.
(* Goal: forall _ : @eq Z Z0 x, Z.le Z0 (Z.mul x y) *)
intros H'1; rewrite <- H'1; simpl in |- *; auto with zarith.
Qed.
Hint Resolve Zle_mult_gen: zarith.
 
Definition Zmax : forall x_ x_ : Z, Z :=
  fun n m : Z =>
  match (n ?= m)%Z with
  | Datatypes.Eq => m
  | Datatypes.Lt => m
  | Datatypes.Gt => n
  end.
 
Theorem ZmaxLe1 : forall z1 z2 : Z, (z1 <= Zmax z1 z2)%Z.
intros z1 z2; unfold Zmax in |- *; CaseEq (z1 ?= z2)%Z; simpl in |- *;
 auto with zarith.
(* Goal: forall _ : @eq comparison (Z.compare z1 z2) Eq, Z.le z1 z2 *)
unfold Zle in |- *; intros H; rewrite H; red in |- *; intros; discriminate.
Qed.
 
Theorem ZmaxSym : forall z1 z2 : Z, Zmax z1 z2 = Zmax z2 z1.
intros z1 z2; unfold Zmax in |- *; CaseEq (z1 ?= z2)%Z; CaseEq (z2 ?= z1)%Z;
 intros H1 H2; try case (Zcompare_EGAL _ _ H1); auto;
 try case (Zcompare_EGAL _ _ H2); auto; Contradict H1.
(* Goal: not (@eq comparison (Z.compare z2 z1) Lt) *)
(* Goal: not (@eq comparison (Z.compare z2 z1) Gt) *)
case (Zcompare.Zcompare_Gt_Lt_antisym z2 z1); auto.
(* Goal: forall (_ : forall _ : @eq comparison (Z.compare z2 z1) Gt, @eq comparison (Z.compare z1 z2) Lt) (_ : forall _ : @eq comparison (Z.compare z1 z2) Lt, @eq comparison (Z.compare z2 z1) Gt), not (@eq comparison (Z.compare z2 z1) Lt) *)
(* Goal: not (@eq comparison (Z.compare z2 z1) Gt) *)
intros H' H'0; rewrite H'0; auto; red in |- *; intros; discriminate.
(* Goal: not (@eq comparison (Z.compare z2 z1) Gt) *)
case (Zcompare.Zcompare_Gt_Lt_antisym z1 z2); auto.
(* Goal: forall (_ : forall _ : @eq comparison (Z.compare z1 z2) Gt, @eq comparison (Z.compare z2 z1) Lt) (_ : forall _ : @eq comparison (Z.compare z2 z1) Lt, @eq comparison (Z.compare z1 z2) Gt), not (@eq comparison (Z.compare z2 z1) Gt) *)
intros H'; rewrite H'; auto; intros; red in |- *; intros; discriminate.
Qed.
 
Theorem Zmax_le2 : forall z1 z2 : Z, (z1 <= z2)%Z -> Zmax z1 z2 = z2.
(* Goal: forall (z1 z2 : Z) (_ : Z.le z1 z2), @eq Z (Zmax z1 z2) z2 *)
intros z1 z2; unfold Zle, Zmax in |- *; case (z1 ?= z2)%Z; auto.
(* Goal: forall _ : not (@eq comparison Gt Gt), @eq Z z1 z2 *)
intros H'; case H'; auto.
Qed.
 
Theorem Zmax_le1 : forall z1 z2 : Z, (z2 <= z1)%Z -> Zmax z1 z2 = z1.
(* Goal: forall (z1 z2 : Z) (_ : Z.le z2 z1), @eq Z (Zmax z1 z2) z1 *)
intros z1 z2 H'; rewrite ZmaxSym; apply Zmax_le2; auto.
Qed.
 
Theorem ZmaxLe2 : forall z1 z2 : Z, (z2 <= Zmax z1 z2)%Z.
(* Goal: forall z1 z2 : Z, Z.le z2 (Zmax z1 z2) *)
intros z1 z2; rewrite ZmaxSym; apply ZmaxLe1.
Qed.
Hint Resolve ZmaxLe1 ZmaxLe2: zarith.
 
Theorem Zeq_Zs :
 forall p q : Z, (p <= q)%Z -> (q < Zsucc p)%Z -> p = q.
(* Goal: forall (p q : Z) (_ : Z.le p q) (_ : Z.lt q (Z.succ p)), @eq Z p q *)
intros p q H' H'0; apply Zle_antisym; auto.
(* Goal: Z.le q p *)
apply Zlt_succ_le; auto.
Qed.
 
Theorem Zmin_Zmax : forall z1 z2 : Z, (Zmin z1 z2 <= Zmax z1 z2)%Z.
intros z1 z2; case (Zle_or_lt z1 z2); unfold Zle, Zlt, Zmin, Zmax in |- *;
 CaseEq (z1 ?= z2)%Z; auto; intros H1 H2; try rewrite H1; 
 try rewrite H2; red in |- *; intros; discriminate.
Qed.
 
Theorem Zabs_Zmult :
 forall z1 z2 : Z, Zabs (z1 * z2) = (Zabs z1 * Zabs z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.lt (Z.opp z2) z1) (_ : Z.lt z1 z2), Z.lt (Z.abs z1) z2 *)
intros z1 z2; case z1; case z2; simpl in |- *; auto with zarith.
Qed.
 
Theorem Zle_Zmult_comp_r :
 forall x y z : Z, (0 <= z)%Z -> (x <= y)%Z -> (x * z <= y * z)%Z.
(* Goal: forall (x y z : Z) (_ : Z.le Z0 z) (_ : Z.le x y), Z.le (Z.mul x z) (Z.mul y z) *)
intros x y z H' H'0; case (Zle_lt_or_eq _ _ H'); intros Zlt1.
(* Goal: Z.le (Z.mul x z) (Z.mul y z) *)
(* Goal: Z.le (Z.mul x z) (Z.mul y z) *)
apply Zmult_gt_0_le_compat_r; auto.
(* Goal: Z.gt z Z0 *)
(* Goal: Z.le (Z.mul x z) (Z.mul y z) *)
apply Zlt_gt; auto.
(* Goal: Z.le (Z.mul x z) (Z.mul y z) *)
rewrite <- Zlt1; repeat rewrite <- Zmult_0_r_reverse; auto with zarith.
Qed.
 
Theorem Zle_Zmult_comp_l :
 forall x y z : Z, (0 <= z)%Z -> (x <= y)%Z -> (z * x <= z * y)%Z.
intros x y z H' H'0; repeat rewrite (Zmult_comm z);
 apply Zle_Zmult_comp_r; auto.
Qed.
 
Theorem NotZmultZero :
 forall z1 z2 : Z, z1 <> 0%Z -> z2 <> 0%Z -> (z1 * z2)%Z <> 0%Z.
(* Goal: forall (z1 z2 : Z) (_ : not (@eq Z z1 Z0)) (_ : not (@eq Z z2 Z0)), not (@eq Z (Z.mul z1 z2) Z0) *)
intros z1 z2; case z1; case z2; simpl in |- *; intros; auto; try discriminate.
Qed.
Hint Resolve NotZmultZero: zarith.
(* Conversions from R <-> Z  <-> N *)
 
Theorem IZR_zero : forall p : Z, p = 0%Z -> IZR p = 0%R.
(* Goal: forall (p : Z) (_ : @eq Z p Z0), @eq R (IZR p) (IZR Z0) *)
intros p H'; rewrite H'; auto.
Qed.
Hint Resolve not_O_INR: real.
 
Theorem IZR_zero_r : forall p : Z, IZR p = 0%R -> p = 0%Z.
(* Goal: forall (p : Z) (_ : @eq R (IZR p) (IZR Z0)), @eq Z p Z0 *)
intros p; case p; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : @eq R (IZR (Zpos p)) (IZR Z0)), @eq Z (Zpos p) Z0 *)
(* Goal: forall (p : positive) (_ : @eq R (IZR (Zneg p)) (IZR Z0)), @eq Z (Zneg p) Z0 *)
intros p1 H'; Contradict H'; auto with real zarith.
(* Goal: forall (p : positive) (_ : @eq R (IZR (Zneg p)) (IZR Z0)), @eq Z (Zneg p) Z0 *)
intros p1 H'; absurd (INR (nat_of_P p1) = 0%R); auto with real zarith.
(* Goal: @eq R (INR (Pos.to_nat p1)) (IZR Z0) *)
rewrite <- (Ropp_involutive (INR (nat_of_P p1))).
(* Goal: @eq R (Ropp (Ropp (INR (Pos.to_nat p1)))) (IZR Z0) *)
unfold IZR in H'; rewrite <- INR_IPR in H'.
(* Goal: @eq R (Ropp (Ropp (INR (Pos.to_nat p1)))) (IZR Z0) *)
rewrite H'; auto with real.
Qed.
 
Theorem INR_lt_nm : forall n m : nat, n < m -> (INR n < INR m)%R.
(* Goal: forall (n m : nat) (_ : lt n m), Rlt (INR n) (INR m) *)
intros n m H'; elim H'; auto.
replace (INR n) with (INR n + 0)%R; auto with real; rewrite S_INR;
 auto with real.
(* Goal: forall (m : nat) (_ : le (S n) m) (_ : Rlt (INR n) (INR m)), Rlt (INR n) (INR (S m)) *)
intros m0 H'0 H'1.
replace (INR n) with (INR n + 0)%R; auto with real; rewrite S_INR;
 auto with real.
Qed.
Hint Resolve INR_lt_nm: real.
 
Theorem Rlt_INR1 : forall n : nat, 1 < n -> (1 < INR n)%R.
(* Goal: forall (n : nat) (_ : not (@eq nat n (S O))), not (@eq R (INR n) (IZR (Zpos xH))) *)
replace 1%R with (INR 1); auto with real.
Qed.
Hint Resolve Rlt_INR1: real.
 
Theorem NEq_INR : forall n m : nat, n <> m -> INR n <> INR m.
(* Goal: forall (n m : nat) (_ : not (@eq nat n m)), not (@eq R (INR n) (INR m)) *)
intros n m H'; (case (le_or_lt n m); intros H'1).
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
case (le_lt_or_eq _ _ H'1); intros H'2.
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
apply Rlt_dichotomy_converse; auto with real.
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
Contradict H'; auto.
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
apply Compare.not_eq_sym; apply Rlt_dichotomy_converse; auto with real.
Qed.
Hint Resolve NEq_INR: real.
 
Theorem NEq_INRO : forall n : nat, n <> 0 -> INR n <> 0%R.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), not (@eq R (INR n) (IZR Z0)) *)
replace 0%R with (INR 0); auto with real.
Qed.
Hint Resolve NEq_INRO: real.
 
Theorem NEq_INR1 : forall n : nat, n <> 1 -> INR n <> 1%R.
(* Goal: forall (n : nat) (_ : not (@eq nat n (S O))), not (@eq R (INR n) (IZR (Zpos xH))) *)
replace 1%R with (INR 1); auto with real.
Qed.
Hint Resolve NEq_INR1: real.
 
Theorem not_O_lt : forall n : nat, n <> 0 -> 0 < n.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros n; elim n; simpl in |- *; auto with arith.
Qed.
Hint Resolve not_O_lt: arith.
 
Theorem NEq_IZRO : forall n : Z, n <> 0%Z -> IZR n <> 0%R.
(* Goal: forall (n : Z) (_ : not (@eq Z n Z0)), not (@eq R (IZR n) (IZR Z0)) *)
intros n H; Contradict H.
(* Goal: @eq Z n Z0 *)
apply IZR_zero_r; auto.
Qed.
Hint Resolve NEq_IZRO: real.
 
Theorem Rlt_IZR : forall p q : Z, (p < q)%Z -> (IZR p < IZR q)%R.
(* Goal: forall (p q : Z) (_ : Z.lt p q), Rlt (IZR p) (IZR q) *)
intros p q H; case (Rle_or_lt (IZR q) (IZR p)); auto.
(* Goal: forall _ : Rle (IZR q) (IZR p), Rlt (IZR p) (IZR q) *)
intros H1; Contradict H; apply Zle_not_lt.
(* Goal: Z.le q p *)
apply le_IZR; auto.
Qed.
Hint Resolve Rlt_IZR: real.
 
Theorem Rle_IZR : forall x y : Z, (x <= y)%Z -> (IZR x <= IZR y)%R.
(* Goal: forall (x y : Z) (_ : Z.le x y), Rle (IZR x) (IZR y) *)
intros x y H'.
(* Goal: Rle (IZR x) (IZR y) *)
case (Zle_lt_or_eq _ _ H'); clear H'; intros H'.
(* Goal: Rle (IZR x) (IZR y) *)
(* Goal: Rle (IZR x) (IZR y) *)
apply Rlt_le; auto with real.
(* Goal: Rle (IZR x) (IZR y) *)
rewrite <- H'; auto with real.
Qed.
Hint Resolve Rle_IZR: real.
 
Theorem Rlt_IZRO : forall p : Z, (0 < p)%Z -> (0 < IZR p)%R.
(* Goal: forall (p : Z) (_ : Z.lt Z0 p), Rlt (IZR Z0) (IZR p) *)
intros p H; replace 0%R with (IZR 0); auto with real.
Qed.
Hint Resolve Rlt_IZRO: real.
 
Theorem Rle_IZRO : forall x y : Z, (0 <= y)%Z -> (0 <= IZR y)%R.
(* Goal: forall (_ : Z) (y : Z) (_ : Z.le Z0 y), Rle (IZR Z0) (IZR y) *)
intros; replace 0%R with (IZR 0); auto with real.
Qed.
Hint Resolve Rle_IZRO: real.
 
Theorem Rlt_IZR1 : forall p q : Z, (1 < q)%Z -> (1 < IZR q)%R.
(* Goal: forall (_ : Z) (y : Z) (_ : Z.le (Zpos xH) y), Rle (IZR (Zpos xH)) (IZR y) *)
intros; replace 1%R with (IZR 1); auto with real.
Qed.
Hint Resolve Rlt_IZR1: real.
 
Theorem Rle_IZR1 : forall x y : Z, (1 <= y)%Z -> (1 <= IZR y)%R.
(* Goal: forall (_ : Z) (y : Z) (_ : Z.le (Zpos xH) y), Rle (IZR (Zpos xH)) (IZR y) *)
intros; replace 1%R with (IZR 1); auto with real.
Qed.
Hint Resolve Rle_IZR1: real.
 
Theorem lt_Rlt : forall n m : nat, (INR n < INR m)%R -> n < m.
intros n m H'; case (le_or_lt m n); auto; intros H0; Contradict H';
 auto with real.
(* Goal: not (Rlt (INR n) (INR m)) *)
case (le_lt_or_eq _ _ H0); intros H1; auto with real.
(* Goal: not (Rlt (INR n) (INR m)) *)
rewrite H1; apply Rlt_irrefl.
Qed.
 
Theorem INR_inv : forall n m : nat, INR n = INR m -> n = m.
(* Goal: forall (n m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m *)
intros n; elim n; auto; try rewrite S_INR.
(* Goal: forall (m : nat) (_ : @eq R (INR O) (INR m)), @eq nat O m *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
intros m; case m; auto.
(* Goal: forall (n : nat) (_ : @eq R (INR O) (INR (S n))), @eq nat O (S n) *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
intros m' H1; Contradict H1; auto.
(* Goal: not (@eq R (INR (S n')) (INR O)) *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
rewrite S_INR.
(* Goal: not (@eq R (INR O) (Rplus (INR m') (IZR (Zpos xH)))) *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
apply Rlt_dichotomy_converse; left.
(* Goal: Rlt (INR O) (Rplus (INR m') (IZR (Zpos xH))) *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
apply Rle_lt_0_plus_1.
(* Goal: Rle (IZR Z0) (INR n') *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
apply pos_INR.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
intros n' H' m; case m.
(* Goal: forall _ : @eq R (INR (S n')) (INR O), @eq nat (S n') O *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
intros H'0; Contradict H'0; auto.
(* Goal: not (@eq R (INR (S n')) (INR O)) *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
rewrite S_INR.
(* Goal: not (@eq R (Rplus (INR n') (IZR (Zpos xH))) (INR O)) *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
apply Rlt_dichotomy_converse; right.
(* Goal: Rlt (INR O) (Rplus (INR m') (IZR (Zpos xH))) *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : @eq R (INR n) (INR m)), @eq nat n m) (m : nat) (_ : @eq R (INR (S n)) (INR m)), @eq nat (S n) m *)
red in |- *; apply Rle_lt_0_plus_1.
(* Goal: Rle (IZR Z0) (INR n') *)
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
apply pos_INR.
(* Goal: forall (n : nat) (_ : @eq R (INR (S n')) (INR (S n))), @eq nat (S n') (S n) *)
intros m' H'0.
(* Goal: @eq nat (S n') (S m') *)
rewrite (H' m'); auto.
(* Goal: @eq R (INR n') (INR m') *)
repeat rewrite S_INR in H'0.
apply Rplus_eq_reg_l with (r := 1%R); repeat rewrite (Rplus_comm 1);
 auto with real.
Qed.
 
Theorem Rle_INR : forall x y : nat, x <= y -> (INR x <= INR y)%R.
(* Goal: forall (x y : nat) (_ : le x y), Rle (INR x) (INR y) *)
intros x y H; repeat rewrite INR_IZR_INZ.
(* Goal: Rle (IZR (Z.of_nat x)) (IZR (Z.of_nat y)) *)
apply Rle_IZR; auto with zarith.
Qed.
Hint Resolve Rle_INR: real.
 
Theorem le_Rle : forall n m : nat, (INR n <= INR m)%R -> n <= m.
(* Goal: forall (n m : nat) (_ : Rle (INR n) (INR m)), le n m *)
intros n m H'; case H'; auto.
(* Goal: forall _ : Rlt (INR n) (INR m), le n m *)
(* Goal: forall _ : @eq R (INR n) (INR m), le n m *)
intros H'0; apply lt_le_weak; apply lt_Rlt; auto.
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
intros H'0; rewrite <- (INR_inv _ _ H'0); auto with arith.
Qed.
 
Theorem Rmult_IZR : forall z t : Z, IZR (z * t) = (IZR z * IZR t)%R.
(* Goal: forall z t : Z, @eq R (IZR (Z.mul z t)) (Rmult (IZR z) (IZR t)) *)
intros z t; case z; case t; simpl in |- *; auto with real; unfold IZR; intros t1 z1; repeat rewrite <- INR_IPR.
- rewrite nat_of_P_mult_morphism; auto with real.
- rewrite nat_of_P_mult_morphism; auto with real.
(* Goal: @eq R (Ropp (INR (Init.Nat.mul (Pos.to_nat z1) (Pos.to_nat t1)))) (Rmult (INR (Pos.to_nat z1)) (Ropp (INR (Pos.to_nat t1)))) *)
  rewrite Rmult_comm.
(* Goal: @eq R (Ropp (INR (Init.Nat.mul (Pos.to_nat z1) (Pos.to_nat t1)))) (Rmult (Ropp (INR (Pos.to_nat z1))) (INR (Pos.to_nat t1))) *)
  rewrite Ropp_mult_distr_l_reverse; auto with real.
(* Goal: @eq R (Ropp (INR (Init.Nat.mul (Pos.to_nat z1) (Pos.to_nat t1)))) (Ropp (Rmult (INR (Pos.to_nat t1)) (INR (Pos.to_nat z1)))) *)
  apply Ropp_eq_compat; rewrite mult_comm; auto with real.
- rewrite nat_of_P_mult_morphism; auto with real.
(* Goal: @eq R (Ropp (INR (Init.Nat.mul (Pos.to_nat z1) (Pos.to_nat t1)))) (Rmult (Ropp (INR (Pos.to_nat z1))) (INR (Pos.to_nat t1))) *)
  rewrite Ropp_mult_distr_l_reverse; auto with real.
- rewrite nat_of_P_mult_morphism; auto with real.
(* Goal: @eq R (INR (Init.Nat.mul (Pos.to_nat z1) (Pos.to_nat t1))) (Rmult (Ropp (INR (Pos.to_nat z1))) (Ropp (INR (Pos.to_nat t1)))) *)
  rewrite Rmult_opp_opp; auto with real.
Qed.
 
Theorem absolu_Zs :
 forall z : Z, (0 <= z)%Z -> Zabs_nat (Zsucc z) = S (Zabs_nat z).
intros z; case z.
3: intros p H'; Contradict H'; auto with zarith.
replace (Zsucc 0) with (Z_of_nat 1).
intros H'; rewrite absolu_INR; simpl in |- *; auto.
simpl in |- *; auto.
intros p H'; rewrite <- Zpos_succ_morphism; simpl in |- *; auto with zarith.
unfold nat_of_P in |- *; rewrite Pmult_nat_succ_morphism; auto.
Qed.
Hint Resolve Zlt_le_succ: zarith.
 
Theorem Zlt_next :
 forall n m : Z, (n < m)%Z -> m = Zsucc n \/ (Zsucc n < m)%Z.
(* Goal: forall (n m : Z) (_ : Z.lt n m), or (@eq Z m (Z.succ n)) (Z.lt (Z.succ n) m) *)
intros n m H'; case (Zle_lt_or_eq (Zsucc n) m); auto with zarith.
Qed.
 
Theorem Zle_next :
 forall n m : Z, (n <= m)%Z -> m = n \/ (Zsucc n <= m)%Z.
(* Goal: forall (n m : Z) (_ : Z.le n m), or (@eq Z m n) (Z.le (Z.succ n) m) *)
intros n m H'; case (Zle_lt_or_eq _ _ H'); auto with zarith.
Qed.
 
Theorem Zlt_Zopp_Inv : forall p q : Z, (- p < - q)%Z -> (q < p)%Z.
(* Goal: forall (p q : Z) (_ : Z.lt (Z.opp p) (Z.opp q)), Z.lt q p *)
intros x y H'; case (Zle_or_lt x y); auto with zarith.
Qed.
 
Theorem Zle_Zopp_Inv : forall p q : Z, (- p <= - q)%Z -> (q <= p)%Z.
(* Goal: forall (p q : Z) (_ : Z.le (Z.opp p) (Z.opp q)), Z.le q p *)
intros p q H'; case (Zle_lt_or_eq _ _ H'); auto with zarith.
Qed.
 
Theorem absolu_Zs_neg :
 forall z : Z, (z < 0)%Z -> S (Zabs_nat (Zsucc z)) = Zabs_nat z.
(* Goal: forall (z : Z) (_ : Z.lt z Z0), @eq nat (S (Z.abs_nat (Z.succ z))) (Z.abs_nat z) *)
intros z H'; apply inject_nat_eq.
(* Goal: @eq Z (Z.of_nat (S (Z.abs_nat (Z.succ z)))) (Z.of_nat (Z.abs_nat z)) *)
rewrite inj_S.
repeat rewrite <- (absolu_Zopp (Zsucc z)).
repeat rewrite <- (absolu_Zopp z).
repeat rewrite inj_abs; replace 0%Z with (- (0))%Z; auto with zarith.
Qed.
 
Theorem Zlt_absolu :
 forall (x : Z) (n : nat), Zabs_nat x < n -> (x < Z_of_nat n)%Z.
intros x n; case x; simpl in |- *; auto with zarith.
(* Goal: forall (p : positive) (_ : lt (Pos.to_nat p) n), Z.lt (Zpos p) (Z.of_nat n) *)
(* Goal: forall (p : positive) (_ : lt (Pos.to_nat p) n), Z.lt (Zneg p) (Z.of_nat n) *)
replace 0%Z with (Z_of_nat 0); auto with zarith.
intros p; rewrite <- (inject_nat_convert (Zpos p) p); auto with zarith.
case n; simpl in |- *; intros; red in |- *; simpl in |- *; auto.
Qed.
 
Theorem inj_pred :
 forall n : nat, n <> 0 -> Z_of_nat (pred n) = Zpred (Z_of_nat n).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @eq Z (Z.of_nat (Init.Nat.pred n)) (Z.pred (Z.of_nat n)) *)
intros n; case n; auto.
(* Goal: not (@eq R (INR n) (INR m)) *)
(* Goal: not (@eq R (INR n) (INR m)) *)
intros H'; Contradict H'; auto.
intros n0 H'; rewrite inj_S; rewrite <- Zpred_succ; auto.
Qed.
 
Theorem Zle_abs : forall p : Z, (p <= Z_of_nat (Zabs_nat p))%Z.
intros p; case p; simpl in |- *; auto with zarith; intros q;
 rewrite inject_nat_convert with (p := Zpos q); 
 auto with zarith.
unfold Zle in |- *; red in |- *; intros H'2; discriminate.
Qed.
Hint Resolve Zle_abs: zarith.
 
Theorem ZleAbs :
 forall (z : Z) (n : nat),
 (- Z_of_nat n <= z)%Z -> (z <= Z_of_nat n)%Z -> Zabs_nat z <= n.
(* Goal: forall (z : Z) (n : nat) (_ : Z.le (Z.opp (Z.of_nat n)) z) (_ : Z.le z (Z.of_nat n)), le (Z.abs_nat z) n *)
intros z n H' H'0; case (le_or_lt (Zabs_nat z) n); auto; intros lt.
(* Goal: le (Z.abs_nat z) n *)
case (Zle_or_lt 0 z); intros Zle0.
(* Goal: le (Z.abs_nat z) n *)
(* Goal: le (Z.abs_nat z) n *)
Contradict H'0.
(* Goal: not (Z.le (Z.opp (Z.of_nat n)) z) *)
apply Zlt_not_le; auto.
rewrite <- (inj_abs z); auto with zarith.
(* Goal: lt n m *)
Contradict H'.
(* Goal: not (Z.le (Z.opp (Z.of_nat n)) z) *)
apply Zlt_not_le; auto.
replace z with (- Z_of_nat (Zabs_nat z))%Z.
(* Goal: Z.lt (Z.opp (Z.of_nat (Z.abs_nat z))) (Z.opp (Z.of_nat n)) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat z))) z *)
apply Zlt_Zopp; auto with zarith.
rewrite <- absolu_Zopp.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat (Z.opp z)))) z *)
rewrite inj_abs; auto with zarith.
Qed.
 
Theorem lt_Zlt_inv : forall n m : nat, (Z_of_nat n < Z_of_nat m)%Z -> n < m.
(* Goal: forall (n m : nat) (_ : Z.lt (Z.of_nat n) (Z.of_nat m)), lt n m *)
intros n m H'; case (le_or_lt n m); auto.
(* Goal: forall _ : le n m, lt n m *)
(* Goal: forall _ : lt m n, lt n m *)
intros H'0.
(* Goal: lt n m *)
(* Goal: forall _ : lt m n, lt n m *)
case (le_lt_or_eq _ _ H'0); auto with zarith.
(* Goal: forall _ : lt m n, lt n m *)
intros H'1.
(* Goal: lt n m *)
Contradict H'.
(* Goal: not (Z.lt (Z.of_nat n) (Z.of_nat m)) *)
apply Zle_not_lt; auto with zarith.
Qed.
 
Theorem NconvertO : forall p : positive, nat_of_P p <> 0.
intros p; elim p; unfold nat_of_P in |- *; simpl in |- *.
(* Goal: forall _ : @eq nat (S n0) O, @eq nat (Init.Nat.sub n0 O) O *)
intros p0 H'; red in |- *; intros H'0; discriminate.
intros p0; rewrite ZL6; unfold nat_of_P in |- *.
case (Pmult_nat p0 1); simpl in |- *; auto.
red in |- *; intros H'; discriminate.
Qed.
Hint Resolve NconvertO: zarith.
 
Theorem absolu_lt_nz : forall z : Z, z <> 0%Z -> 0 < Zabs_nat z.
intros z; case z; simpl in |- *; auto; try (intros H'; case H'; auto; fail);
(* Goal: forall (q r : nat) (_ : lt O O) (_ : lt q r), lt O O *)
(* Goal: forall (n : nat) (_ : forall (q r : nat) (_ : lt O n) (_ : lt q r), lt (Init.Nat.mul n q) (Init.Nat.mul n r)) (q r : nat) (_ : lt O (S n)) (_ : lt q r), lt (Init.Nat.add q (Init.Nat.mul n q)) (Init.Nat.add r (Init.Nat.mul n r)) *)
 intros p; generalize (NconvertO p); auto with arith.
Qed.
 
Theorem Rlt2 : (0 < INR 2)%R.
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
replace 0%R with (INR 0); auto with real arith.
Qed.
Hint Resolve Rlt2: real.
 
Theorem RlIt2 : (0 < / INR 2)%R.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) r) r *)
apply Rmult_lt_reg_l with (r := INR 2); auto with real.
Qed.
Hint Resolve RlIt2: real.
 
Theorem Rledouble : forall r : R, (0 <= r)%R -> (r <= INR 2 * r)%R.
(* Goal: forall (r : R) (_ : Rlt (IZR Z0) r), Rlt (Rmult (Rinv (INR (S (S O)))) r) r *)
intros r H'.
replace (INR 2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
pattern r at 1 in |- *; replace r with (r + 0)%R; [ idtac | ring ].
(* Goal: Rle (Rplus r (IZR Z0)) (Rplus r r) *)
apply Rplus_le_compat_l; auto.
Qed.
 
Theorem Rltdouble : forall r : R, (0 < r)%R -> (r < INR 2 * r)%R.
(* Goal: forall (r : R) (_ : Rlt (IZR Z0) r), Rlt (Rmult (Rinv (INR (S (S O)))) r) r *)
intros r H'.
pattern r at 1 in |- *; replace r with (r + 0)%R; try ring.
replace (INR 2 * r)%R with (r + r)%R; simpl in |- *; try ring; auto with real.
Qed.
 
Theorem Rlt_RinvDouble : forall r : R, (0 < r)%R -> (/ INR 2 * r < r)%R.
(* Goal: forall (r : R) (_ : Rlt (IZR Z0) r), Rlt (Rmult (Rinv (INR (S (S O)))) r) r *)
intros r H'.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) r) r *)
apply Rmult_lt_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) r) (Rmult (INR (S (S O))) r) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
apply Rmult_lt_compat_r; replace 1%R with (INR 1); auto with real arith.
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
replace 0%R with (INR 0); auto with real arith.
Qed.
Hint Resolve Rledouble: real.
 
Theorem Rle_Rinv : forall x y : R, (0 < x)%R -> (x <= y)%R -> (/ y <= / x)%R.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x y), Rle (Rinv y) (Rinv x) *)
intros x y H H1; case H1; intros H2.
(* Goal: Rle (Rinv y) (Rinv x) *)
(* Goal: Rle (Rinv y) (Rinv x) *)
left; apply Rinv_lt_contravar; auto.
(* Goal: Rlt (IZR Z0) (Rmult x y) *)
(* Goal: Rle (Rinv y) (Rinv x) *)
apply Rmult_lt_0_compat; auto.
(* Goal: Rlt (IZR Z0) y *)
(* Goal: Rle (Rinv y) (Rinv x) *)
apply Rlt_trans with (2 := H2); auto.
(* Goal: Rle (Rinv y) (Rinv x) *)
rewrite H2; auto with real.
Qed.
 
Theorem Int_part_INR : forall n : nat, Int_part (INR n) = Z_of_nat n.
intros n; unfold Int_part in |- *.
(* Goal: @eq Z (Z.sub (up (INR n)) (Zpos xH)) (Z.of_nat n) *)
cut (up (INR n) = (Z_of_nat n + Z_of_nat 1)%Z).
intros H'; rewrite H'; simpl in |- *; ring.
(* Goal: @eq Z (up (INR n)) (Z.add (Z.of_nat n) (Z.of_nat (S O))) *)
apply sym_equal; apply tech_up; auto.
(* Goal: Rlt (INR n) (IZR (Z.add (Z.of_nat n) (Z.of_nat (S O)))) *)
(* Goal: Rle (IZR (Z.add (Z.of_nat n) (Z.of_nat (S O)))) (Rplus (INR n) (IZR (Zpos xH))) *)
replace (Z_of_nat n + Z_of_nat 1)%Z with (Z_of_nat (S n)).
repeat rewrite <- INR_IZR_INZ.
(* Goal: Rlt (INR n) (INR (S n)) *)
(* Goal: @eq Z (Z.of_nat (S n)) (Z.add (Z.of_nat n) (Z.of_nat (S O))) *)
(* Goal: Rle (IZR (Z.add (Z.of_nat n) (Z.of_nat (S O)))) (Rplus (INR n) (IZR (Zpos xH))) *)
apply INR_lt_nm; auto.
rewrite Zplus_comm; rewrite <- inj_plus; simpl in |- *; auto.
rewrite plus_IZR; simpl in |- *; auto with real.
repeat rewrite <- INR_IZR_INZ; auto with real.
Qed.
 
Theorem Int_part_IZR : forall z : Z, Int_part (IZR z) = z.
intros z; unfold Int_part in |- *.
(* Goal: @eq Z (Z.sub (up (IZR z)) (Zpos xH)) z *)
cut (up (IZR z) = (z + 1)%Z).
intros Z1; rewrite Z1; rewrite Zplus_comm; apply Zminus_plus;
 auto with zarith.
apply sym_equal; apply tech_up; simpl in |- *; auto with real zarith.
replace (IZR z) with (IZR z + IZR 0)%R; try rewrite plus_IZR;
 auto with real zarith.
Qed.
 
Theorem Zlt_Rlt : forall z1 z2 : Z, (IZR z1 < IZR z2)%R -> (z1 < z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Rlt (IZR z1) (IZR z2)), Z.lt z1 z2 *)
intros z1 z2 H; case (Zle_or_lt z2 z1); auto.
(* Goal: forall _ : Z.lt z2 z1, Z.le z1 z2 *)
intros H1; Contradict H; auto with real zarith.
(* Goal: not (Rlt (IZR z1) (IZR z2)) *)
apply Rle_not_lt; auto with real zarith.
Qed.
 
Theorem Zle_Rle :
 forall z1 z2 : Z, (IZR z1 <= IZR z2)%R -> (z1 <= z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Rle (IZR z1) (IZR z2)), Z.le z1 z2 *)
intros z1 z2 H; case (Zle_or_lt z1 z2); auto.
(* Goal: forall _ : Z.lt z2 z1, Z.le z1 z2 *)
intros H1; Contradict H; auto with real zarith.
(* Goal: not (Rle (IZR z1) (IZR z2)) *)
apply Rlt_not_le; auto with real zarith.
Qed.
 
Theorem IZR_inv : forall z1 z2 : Z, IZR z1 = IZR z2 :>R -> z1 = z2.
(* Goal: forall (z1 z2 : Z) (_ : @eq R (IZR z1) (IZR z2)), @eq Z z1 z2 *)
intros z1 z2 H; apply Zle_antisym; apply Zle_Rle; rewrite H; auto with real.
Qed.
 
Theorem Zabs_eq_opp : forall x, (x <= 0)%Z -> Zabs x = (- x)%Z.
intros x; case x; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : Z.le (Zpos p) Z0), @eq Z (Zpos p) (Zneg p) *)
intros p H; Contradict H; auto with zarith.
Qed.
 
Theorem Zabs_Zs : forall z : Z, (Zabs (Zsucc z) <= Zsucc (Zabs z))%Z.
intros z; case z; auto.
simpl in |- *; auto with zarith.
repeat rewrite Zabs_eq; auto with zarith.
intros p; rewrite Zabs_eq_opp; auto with zarith.
2: unfold Zsucc in |- *; replace 0%Z with (-1 + 1)%Z; auto with zarith.
2: case p; simpl in |- *; intros; red in |- *; simpl in |- *; intros;
    red in |- *; intros; discriminate.
replace (- Zsucc (Zneg p))%Z with (Zpos p - 1)%Z.
replace (Zsucc (Zabs (Zneg p))) with (Zpos p + 1)%Z;
 auto with zarith.
unfold Zsucc in |- *; rewrite Zopp_plus_distr.
auto with zarith.
Qed.
Hint Resolve Zabs_Zs: zarith.
 
Theorem Zle_Zpred : forall x y : Z, (x < y)%Z -> (x <= Zpred y)%Z.
(* Goal: forall (x y : Z) (_ : Z.lt x y), Z.le x (Z.pred y) *)
intros x y H; apply Zlt_succ_le.
rewrite <- Zsucc_pred; auto.
Qed.
Hint Resolve Zle_Zpred: zarith.
 
Theorem Zabs_Zopp : forall z : Z, Zabs (- z) = Zabs z.
intros z; case z; simpl in |- *; auto.
Qed.
 
Theorem Zle_Zabs : forall z : Z, (z <= Zabs z)%Z.
intros z; case z; simpl in |- *; red in |- *; simpl in |- *; auto;
 try (red in |- *; intros; discriminate; fail).
intros p; elim p; simpl in |- *; auto;
 try (red in |- *; intros; discriminate; fail).
Qed.
Hint Resolve Zle_Zabs: zarith.
 
Theorem Zlt_mult_simpl_l :
 forall a b c : Z, (0 < c)%Z -> (c * a < c * b)%Z -> (a < b)%Z.
(* Goal: forall (a b c : Z) (_ : Z.lt Z0 c) (_ : Z.lt (Z.mul c a) (Z.mul c b)), Z.lt a b *)
intros a b0 c H H0; apply Zgt_lt.
apply Zmult_gt_reg_r with (p := c); try apply Zlt_gt; auto with zarith.
repeat rewrite (fun x => Zmult_comm x c); auto with zarith.
Qed.
(* An equality function on Z that return a bool *)
 
Fixpoint pos_eq_bool (a b : positive) {struct b} : bool :=
  match a, b with
  | xH, xH => true
  | xI a', xI b' => pos_eq_bool a' b'
  | xO a', xO b' => pos_eq_bool a' b'
  | _, _ => false
  end.
 
Theorem pos_eq_bool_correct :
 forall p q : positive,
 match pos_eq_bool p q with
 | true => p = q
 | false => p <> q
 end.
intros p q; generalize p; elim q; simpl in |- *; auto; clear p q.
intros p Rec q; case q; simpl in |- *;
 try (intros; red in |- *; intros; discriminate; fail).
intros q'; generalize (Rec q'); case (pos_eq_bool q' p); simpl in |- *; auto.
(* Goal: forall _ : @eq positive q' p', @eq Z (Zneg q') (Zneg p') *)
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; rewrite H1; auto.
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; Contradict H1; injection H1; auto.
intros p Rec q; case q; simpl in |- *;
 try (intros; red in |- *; intros; discriminate; fail).
intros q'; generalize (Rec q'); case (pos_eq_bool q' p); simpl in |- *; auto.
(* Goal: forall _ : @eq positive q' p', @eq Z (Zneg q') (Zneg p') *)
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; rewrite H1; auto.
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; Contradict H1; injection H1; auto.
intros q; case q; simpl in |- *;
 try (intros; red in |- *; intros; discriminate; fail); 
 auto.
Qed.
 
Theorem Z_O_1 : (0 < 1)%Z.
red in |- *; simpl in |- *; auto; intros; red in |- *; intros; discriminate.
Qed.
Hint Resolve Z_O_1: zarith.
 
Definition Z_eq_bool a b :=
  match a, b with
  | Z0, Z0 => true
  | Zpos a', Zpos b' => pos_eq_bool a' b'
  | Zneg a', Zneg b' => pos_eq_bool a' b'
  | _, _ => false
  end.
 
Theorem Z_eq_bool_correct :
 forall p q : Z,
 match Z_eq_bool p q with
 | true => p = q
 | false => p <> q
 end.
intros p q; case p; case q; simpl in |- *; auto;
 try (intros; red in |- *; intros; discriminate; fail).
intros p' q'; generalize (pos_eq_bool_correct q' p');
 case (pos_eq_bool q' p'); simpl in |- *; auto.
(* Goal: forall _ : @eq positive q' p', @eq Z (Zneg q') (Zneg p') *)
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; rewrite H1; auto.
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; Contradict H1; injection H1; auto.
intros p' q'; generalize (pos_eq_bool_correct q' p');
 case (pos_eq_bool q' p'); simpl in |- *; auto.
(* Goal: forall _ : @eq positive q' p', @eq Z (Zneg q') (Zneg p') *)
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; rewrite H1; auto.
(* Goal: forall _ : not (@eq positive q' p'), not (@eq Z (Zneg q') (Zneg p')) *)
intros H1; Contradict H1; injection H1; auto.
Qed.
 
Theorem Zlt_mult_ZERO :
 forall x y : Z, (0 < x)%Z -> (0 < y)%Z -> (0 < x * y)%Z.
intros x y; case x; case y; unfold Zlt in |- *; simpl in |- *; auto.
Qed.
Hint Resolve Zlt_mult_ZERO: zarith.
 
Theorem Zlt_Zminus_ZERO :
 forall z1 z2 : Z, (z2 < z1)%Z -> (0 < z1 - z2)%Z.
intros z1 z2; rewrite (Zminus_diag_reverse z2); auto with zarith.
Qed.
 
Theorem Zle_Zminus_ZERO :
 forall z1 z2 : Z, (z2 <= z1)%Z -> (0 <= z1 - z2)%Z.
intros z1 z2; rewrite (Zminus_diag_reverse z2); auto with zarith.
Qed.
Hint Resolve Zle_Zminus_ZERO Zlt_Zminus_ZERO: zarith.
 
Theorem Zle_Zpred_Zpred :
 forall z1 z2 : Z, (z1 <= z2)%Z -> (Zpred z1 <= Zpred z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le z1 z2), Z.le (Z.pred z1) (Z.pred z2) *)
intros z1 z2 H; apply Zsucc_le_reg.
repeat rewrite <- Zsucc_pred; auto.
Qed.
Hint Resolve Zle_Zpred_Zpred: zarith.
 
Theorem Zle_ZERO_Zabs : forall z : Z, (0 <= Zabs z)%Z.
intros z; case z; simpl in |- *; auto with zarith.
Qed.
Hint Resolve Zle_ZERO_Zabs: zarith.
 
Theorem Zlt_Zabs_inv1 :
 forall z1 z2 : Z, (Zabs z1 < z2)%Z -> (- z2 < z1)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le (Z.abs z1) z2), Z.le z1 z2 *)
intros z1 z2 H; case (Zle_or_lt 0 z1); intros H1.
apply Zlt_le_trans with (- (0))%Z; auto with zarith.
apply Zlt_Zopp; apply Zle_lt_trans with (2 := H); auto with zarith.
rewrite <- (Zopp_involutive z1); rewrite <- (Zabs_eq_opp z1);
 auto with zarith.
Qed.
 
Theorem Zlt_Zabs_inv2 :
 forall z1 z2 : Z, (Zabs z1 < Zabs z2)%Z -> (z1 < Zabs z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.lt (Z.opp z2) z1) (_ : Z.lt z1 z2), Z.lt (Z.abs z1) z2 *)
intros z1 z2; case z1; case z2; simpl in |- *; auto with zarith.
Qed.
 
Theorem Zle_Zabs_inv1 :
 forall z1 z2 : Z, (Zabs z1 <= z2)%Z -> (- z2 <= z1)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le (Z.abs z1) z2), Z.le z1 z2 *)
intros z1 z2 H; case (Zle_or_lt 0 z1); intros H1.
apply Zle_trans with (- (0))%Z; auto with zarith.
apply Zle_Zopp; apply Zle_trans with (2 := H); auto with zarith.
rewrite <- (Zopp_involutive z1); rewrite <- (Zabs_eq_opp z1);
 auto with zarith.
Qed.
 
Theorem Zle_Zabs_inv2 :
 forall z1 z2 : Z, (Zabs z1 <= z2)%Z -> (z1 <= z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le (Z.abs z1) z2), Z.le z1 z2 *)
intros z1 z2 H; case (Zle_or_lt 0 z1); intros H1.
rewrite <- (Zabs_eq z1); auto.
apply Zle_trans with (Zabs z1); auto with zarith.
Qed.
 
Theorem Zlt_Zabs_Zpred :
 forall z1 z2 : Z,
 (Zabs z1 < z2)%Z -> z1 <> Zpred z2 -> (Zabs (Zsucc z1) < z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.lt (Z.abs z1) z2) (_ : not (@eq Z z1 (Z.pred z2))), Z.lt (Z.abs (Z.succ z1)) z2 *)
intros z1 z2 H H0; case (Zle_or_lt 0 z1); intros H1.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq in H; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.succ z1)) z2 *)
apply Zlt_trans with (2 := H).
repeat rewrite Zabs_eq_opp; auto with zarith.
Qed.
 
Theorem Zle_n_Zpred :
 forall z1 z2 : Z, (Zpred z1 <= Zpred z2)%Z -> (z1 <= z2)%Z.
intros z1 z2 H; rewrite (Zsucc_pred z1); rewrite (Zsucc_pred z2);
 auto with zarith.
Qed.
 
Theorem Zpred_Zopp_Zs : forall z : Z, Zpred (- z) = (- Zsucc z)%Z.
(* Goal: forall z : Z, @eq Z (Z.pred (Z.opp z)) (Z.opp (Z.succ z)) *)
intros z; unfold Zpred, Zsucc in |- *; ring.
Qed.
 
Theorem Zlt_1_O : forall z : Z, (1 <= z)%Z -> (0 < z)%Z.
intros z H; apply Zsucc_lt_reg; simpl in |- *; auto with zarith.
Qed.
Hint Resolve Zlt_succ Zsucc_lt_compat Zle_lt_succ: zarith.
 
Theorem Zlt_not_eq : forall p q : Z, (p < q)%Z -> p <> q.
intros p q H; Contradict H; rewrite H; auto with zarith.
Qed.
 
Theorem Zlt_not_eq_rev : forall p q : Z, (q < p)%Z -> p <> q.
intros p q H; Contradict H; rewrite H; auto with zarith.
Qed.
Hint Resolve Zlt_not_eq Zlt_not_eq_rev: zarith.
 
Theorem Zle_Zpred_Zlt :
 forall z1 z2 : Z, (z1 <= z2)%Z -> (Zpred z1 < z2)%Z.
intros z1 z2 H; apply Zsucc_lt_reg; rewrite <- Zsucc_pred; auto with zarith.
Qed.
Hint Resolve Zle_Zpred_Zlt: zarith.
 
Theorem Zle_Zpred_inv :
 forall z1 z2 : Z, (z1 <= Zpred z2)%Z -> (z1 < z2)%Z.
intros z1 z2 H; rewrite (Zsucc_pred z2); auto with zarith.
Qed.
 
Theorem Zabs_intro :
 forall (P : Z -> Prop) (z : Z), P (- z)%Z -> P z -> P (Zabs z).
intros P z; case z; simpl in |- *; auto.
Qed.
 
Theorem Zpred_Zle_Zabs_intro :
 forall z1 z2 : Z,
 (- Zpred z2 <= z1)%Z -> (z1 <= Zpred z2)%Z -> (Zabs z1 < z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le (Z.opp (Z.pred z2)) z1) (_ : Z.le z1 (Z.pred z2)), Z.lt (Z.abs z1) z2 *)
intros z1 z2 H H0; apply Zle_Zpred_inv.
apply Zabs_intro with (P := fun x => (x <= Zpred z2)%Z); auto with zarith.
Qed.
 
Theorem Zlt_ZERO_Zle_ONE : forall z : Z, (0 < z)%Z -> (1 <= z)%Z.
intros z H; replace 1%Z with (Zsucc 0); auto with zarith; simpl in |- *; auto.
Qed.
Hint Resolve Zlt_ZERO_Zle_ONE: zarith.
 
Theorem ptonat_def1 : forall p q, 1 < Pmult_nat p (S (S q)).
(* Goal: forall (m : nat) (_ : le p m) (_ : forall _ : le r t, le (Init.Nat.mul p r) (Init.Nat.mul m t)) (_ : le r t), le (Init.Nat.mul p r) (Init.Nat.add t (Init.Nat.mul m t)) *)
intros p; elim p; simpl in |- *; auto with arith.
Qed.
Hint Resolve ptonat_def1: arith.
 
Theorem lt_S_le : forall p q, p < q -> S p <= q.
intros p q; unfold lt in |- *; simpl in |- *; auto.
Qed.
Hint Resolve lt_S_le: arith.
 
Theorem Zlt_Zabs_intro :
 forall z1 z2 : Z, (- z2 < z1)%Z -> (z1 < z2)%Z -> (Zabs z1 < z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.lt (Z.opp z2) z1) (_ : Z.lt z1 z2), Z.lt (Z.abs z1) z2 *)
intros z1 z2; case z1; case z2; simpl in |- *; auto with zarith.
intros p p0 H H0; change (- Zneg p0 < - Zneg p)%Z in |- *;
 auto with zarith.
Qed.
