ArithProp.v

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

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

Require Import Rbase.
Require Import Rbasic_fun.
Require Import Even.
Require Import Div2.
Require Import ArithRing.

Local Open Scope Z_scope.
Local Open Scope R_scope.

Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat.forall n i : nat, (i < n)%nat -> (n - i)%nat <> 0%nat
Proof.forall n i : nat, (i < n)%nat -> (n - i)%nat <> 0%nat
  intros; red; intro.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
False
  cut (forall n m:nat, (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
(forall n0 m : nat,
 (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m) ->
False
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  intro; assert (H2 := H1 _ _ (lt_le_weak _ _ H) H0); rewrite H2 in H;
    elim (lt_irrefl _ H).n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  set (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  cut
    ((forall n m:nat, R n m) ->
      forall n0 m:nat, (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m).n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
((forall n0 m : nat, R n0 m) ->
 forall n0 m : nat,
 (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  intro; apply H1.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 m : nat, R n0 m
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  apply nat_double_ind.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 : nat, R 0%nat n0
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 : nat, R (S n0) 0%nat
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 m : nat, R n0 m -> R (S n0) (S m)
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  unfold R; intros; inversion H2; reflexivity.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 : nat, R (S n0) 0%nat
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 m : nat, R n0 m -> R (S n0) (S m)
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  unfold R; intros; simpl in H3; assumption.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
H1:(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
forall n0 m : nat, R n0 m -> R (S n0) (S m)
n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  unfold R; intros; simpl in H4; assert (H5 := le_S_n _ _ H3);
    assert (H6 := H2 H5 H4); rewrite H6; reflexivity.n, i:nat
H:(i < n)%nat
H0:(n - i)%nat = 0%nat
R:=fun n0 m : nat =>
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m:nat -> nat -> Prop
(forall n0 m : nat, R n0 m) ->
forall n0 m : nat,
(m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m
  unfold R; intros; apply H1; assumption.
Qed.

Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat.forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
Proof.forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  set (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat).R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  cut
    ((forall m n:nat, R m n) -> forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat).R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
((forall m n : nat, R m n) ->
 forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  intro; apply H.R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall m n : nat, R m n
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  apply nat_double_ind.R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n : nat, R 0%nat n
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n : nat, R (S n) 0%nat
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n m : nat, R n m -> R (S n) (S m)
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  unfold R; intros; simpl; apply le_n.R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n : nat, R (S n) 0%nat
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n m : nat, R n m -> R (S n) (S m)
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  unfold R; intros; simpl; apply le_n.R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
H:(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
forall n m : nat, R n m -> R (S n) (S m)
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  unfold R; intros; simpl; apply le_trans with n.R:=fun m0 n0 : nat =>
(n0 <= m0)%nat -> (m0 - n0 <= m0)%nat:nat -> nat -> Prop
H:(forall m0 n0 : nat, R m0 n0) ->
forall n0 i : nat,
(i <= n0)%nat -> (n0 - i <= n0)%nat
n, m:nat
H0:(m <= n)%nat -> (n - m <= n)%nat
H1:(S m <= S n)%nat
(n - m <= n)%nat
R:=fun m0 n0 : nat =>
(n0 <= m0)%nat -> (m0 - n0 <= m0)%nat:nat -> nat -> Prop
H:(forall m0 n0 : nat, R m0 n0) ->
forall n0 i : nat,
(i <= n0)%nat -> (n0 - i <= n0)%nat
n, m:nat
H0:(m <= n)%nat -> (n - m <= n)%nat
H1:(S m <= S n)%nat
(n <= S n)%nat
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  apply H0; apply le_S_n; assumption.R:=fun m0 n0 : nat =>
(n0 <= m0)%nat -> (m0 - n0 <= m0)%nat:nat -> nat -> Prop
H:(forall m0 n0 : nat, R m0 n0) ->
forall n0 i : nat,
(i <= n0)%nat -> (n0 - i <= n0)%nat
n, m:nat
H0:(m <= n)%nat -> (n - m <= n)%nat
H1:(S m <= S n)%nat
(n <= S n)%nat
R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  apply le_n_Sn.R:=fun m n : nat => (n <= m)%nat -> (m - n <= m)%nat:nat -> nat -> Prop
(forall m n : nat, R m n) ->
forall n i : nat, (i <= n)%nat -> (n - i <= n)%nat
  unfold R; intros; apply H; assumption.
Qed.

Lemma lt_minus_O_lt : forall m n:nat, (m < n)%nat -> (0 < n - m)%nat.forall m n : nat, (m < n)%nat -> (0 < n - m)%nat
Proof.forall m n : nat, (m < n)%nat -> (0 < n - m)%nat
  intros n m; pattern n, m; apply nat_double_ind;
    [ intros; rewrite <- minus_n_O; assumption
      | intros; elim (lt_n_O _ H)
      | intros; simpl; apply H; apply lt_S_n; assumption ].
Qed.

Lemma even_odd_cor :
  forall n:nat,  exists p : nat, n = (2 * p)%nat \/ n = S (2 * p).forall n : nat,
exists p : nat, n = (2 * p)%nat \/ n = S (2 * p)
Proof.forall n : nat,
exists p : nat, n = (2 * p)%nat \/ n = S (2 * p)
  intro.n:nat
exists p : nat, n = (2 * p)%nat \/ n = S (2 * p)
  assert (H := even_or_odd n).n:nat
H:even n \/ odd n
exists p : nat, n = (2 * p)%nat \/ n = S (2 * p)
  exists (div2 n).n:nat
H:even n \/ odd n
n = (2 * Nat.div2 n)%nat \/ n = S (2 * Nat.div2 n)
  assert (H0 := even_odd_double n).n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
n = (2 * Nat.div2 n)%nat \/ n = S (2 * Nat.div2 n)
  elim H0; intros.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
n = (2 * Nat.div2 n)%nat \/ n = S (2 * Nat.div2 n)
  elim H1; intros H3 _.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
n = (2 * Nat.div2 n)%nat \/ n = S (2 * Nat.div2 n)
  elim H2; intros H4 _.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
n = (2 * Nat.div2 n)%nat \/ n = S (2 * Nat.div2 n)
  replace (2 * div2 n)%nat with (double (div2 n)).n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
n = Nat.double (Nat.div2 n) \/
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  elim H; intro.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:even n
n = Nat.double (Nat.div2 n) \/
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:odd n
n = Nat.double (Nat.div2 n) \/
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  left.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:even n
n = Nat.double (Nat.div2 n)
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:odd n
n = Nat.double (Nat.div2 n) \/
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  apply H3; assumption.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:odd n
n = Nat.double (Nat.div2 n) \/
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  right.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
H5:odd n
n = S (Nat.double (Nat.div2 n))
n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  apply H4; assumption.n:nat
H:even n \/ odd n
H0:(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
H1:even n <-> n = Nat.double (Nat.div2 n)
H2:odd n <-> n = S (Nat.double (Nat.div2 n))
H3:even n -> n = Nat.double (Nat.div2 n)
H4:odd n -> n = S (Nat.double (Nat.div2 n))
Nat.double (Nat.div2 n) = (2 * Nat.div2 n)%nat
  unfold double;ring.
Qed.

  (* 2m <= 2n => m<=n *)
Lemma le_double : forall m n:nat, (2 * m <= 2 * n)%nat -> (m <= n)%nat.forall m n : nat, (2 * m <= 2 * n)%nat -> (m <= n)%nat
Proof.forall m n : nat, (2 * m <= 2 * n)%nat -> (m <= n)%nat
  intros; apply INR_le.m, n:nat
H:(2 * m <= 2 * n)%nat
INR m <= INR n
  assert (H1 := le_INR _ _ H).m, n:nat
H:(2 * m <= 2 * n)%nat
H1:INR (2 * m) <= INR (2 * n)
INR m <= INR n
  do 2 rewrite mult_INR in H1.m, n:nat
H:(2 * m <= 2 * n)%nat
H1:INR 2 * INR m <= INR 2 * INR n
INR m <= INR n
  apply Rmult_le_reg_l with (INR 2).m, n:nat
H:(2 * m <= 2 * n)%nat
H1:INR 2 * INR m <= INR 2 * INR n
0 < INR 2
m, n:nat
H:(2 * m <= 2 * n)%nat
H1:INR 2 * INR m <= INR 2 * INR n
INR 2 * INR m <= INR 2 * INR n
  replace (INR 2) with 2; [ prove_sup0 | reflexivity ].m, n:nat
H:(2 * m <= 2 * n)%nat
H1:INR 2 * INR m <= INR 2 * INR n
INR 2 * INR m <= INR 2 * INR n
  assumption.
Qed.

Here, we have the euclidian division

This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI

Lemma euclidian_division :
  forall x y:R,
    y <> 0 ->
    exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y).forall x y : R,
y <> 0 ->
exists (k : Z) (r : R),
  x = IZR k * y + r /\ 0 <= r < Rabs y
Proof.forall x y : R,
y <> 0 ->
exists (k : Z) (r : R),
  x = IZR k * y + r /\ 0 <= r < Rabs y
  intros.x, y:R
H:y <> 0
exists (k : Z) (r : R),
  x = IZR k * y + r /\ 0 <= r < Rabs y
  set
    (k0 :=
      match Rcase_abs y with
	| left _ => (1 - up (x / - y))%Z
	| right _ => (up (x / y) - 1)%Z
      end).x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
exists (k : Z) (r : R),
  x = IZR k * y + r /\ 0 <= r < Rabs y
  exists k0.x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
exists r : R, x = IZR k0 * y + r /\ 0 <= r < Rabs y
  exists (x - IZR k0 * y).x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
x = IZR k0 * y + (x - IZR k0 * y) /\
0 <= x - IZR k0 * y < Rabs y
  split.x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
x = IZR k0 * y + (x - IZR k0 * y)
x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
0 <= x - IZR k0 * y < Rabs y
  ring.x, y:R
H:y <> 0
k0:=if Rcase_abs y
then (1 - up (x / - y))%Z
else (up (x / y) - 1)%Z:Z
0 <= x - IZR k0 * y < Rabs y
  unfold k0; case (Rcase_abs y) as [Hlt|Hge].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
0 <= x - IZR (1 - up (x / - y)) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl;
    unfold Rminus.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 <= x + - ((1 + - IZR (up (x / - y))) * y) < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  replace (- ((1 + - IZR (up (x / - y))) * y)) with
    ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 <= x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  split.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 <= x + (IZR (up (x / - y)) - 1) * y
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  apply Rmult_le_reg_l with (/ - y).x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 < / - y
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
/ - y * 0 <=
/ - y * (x + (IZR (up (x / - y)) - 1) * y)
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
/ - y * 0 <=
/ - y * (x + (IZR (up (x / - y)) - 1) * y)
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite Rmult_0_r; rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 <= x * - / y + (IZR (up (x / - y)) - 1) * y * - / y
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
    rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 <= - (x * / y) + - (IZR (up (x / - y)) - 1)
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  apply Rplus_le_reg_l with (IZR (up (x / - y)) - x / - y).x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
IZR (up (x / - y)) - x / - y + 0 <=
IZR (up (x / - y)) - x / - y +
(- (x * / y) + - (IZR (up (x / - y)) - 1))
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite Rplus_0_r; unfold Rdiv; pattern (/ - y) at 4;
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
IZR (up (x * / - y)) - x * / - y <=
IZR (up (x * / - y)) - x * - / y +
(- (x * / y) + - (IZR (up (x * / - y)) - 1))
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  replace
    (IZR (up (x * / - y)) - x * - / y +
      (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1;
    [ idtac | ring ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
IZR (up (x * / - y)) - x * / - y <= 1
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  elim H0; intros _ H1; unfold Rdiv in H1; exact H1.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x + (IZR (up (x / - y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite (Rabs_left _ Hlt); apply Rmult_lt_reg_l with (/ - y).x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
0 < / - y
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
/ - y * (x + (IZR (up (x / - y)) - 1) * y) <
/ - y * - y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
/ - y * (x + (IZR (up (x / - y)) - 1) * y) <
/ - y * - y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite <- Rinv_l_sym.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
/ - y * (x + (IZR (up (x / - y)) - 1) * y) < 1
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
    rewrite <- Ropp_inv_permute; [ idtac | assumption ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
x * - / y + (IZR (up (x / - y)) - 1) * y * - / y < 1
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
    rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ];
      apply Rplus_lt_reg_l with (IZR (up (x / - y)) - 1).x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
IZR (up (x / - y)) - 1 +
(- (x * / y) + - (IZR (up (x / - y)) - 1)) <
IZR (up (x / - y)) - 1 + 1
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  replace (IZR (up (x / - y)) - 1 + 1) with (IZR (up (x / - y)));
    [ idtac | ring ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
IZR (up (x / - y)) - 1 +
(- (x * / y) + - (IZR (up (x / - y)) - 1)) <
IZR (up (x / - y))
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1)))
    with (- (x * / y)); [ idtac | ring ].x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- (x * / y) < IZR (up (x / - y))
x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0;
    unfold Rdiv; intros H1 _; exact H1.x, y:R
H:y <> 0
Hlt:y < 0
k0:=(1 - up (x / - y))%Z:Z
H0:IZR (up (x / - y)) > x / - y /\
IZR (up (x / - y)) - x / - y <= 1
- y <> 0
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  apply Ropp_neq_0_compat; assumption.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
0 <= x - IZR (up (x / y) - 1) * y < Rabs y
  assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl;
    cut (0 < y).x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y -> 0 <= x - (IZR (up (x / y)) - 1) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  intro; unfold Rminus;
    replace (- ((IZR (up (x / y)) + -(1)) * y)) with ((1 - IZR (up (x / y))) * y);
      [ idtac | ring ].x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
0 <= x + (1 - IZR (up (x / y))) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  split.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
0 <= x + (1 - IZR (up (x / y))) * y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
x + (1 - IZR (up (x / y))) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  apply Rmult_le_reg_l with (/ y).x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
0 < / y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
/ y * 0 <= / y * (x + (1 - IZR (up (x / y))) * y)
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
x + (1 - IZR (up (x / y))) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  apply Rinv_0_lt_compat; assumption.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
/ y * 0 <= / y * (x + (1 - IZR (up (x / y))) * y)
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
x + (1 - IZR (up (x / y))) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  rewrite Rmult_0_r; rewrite (Rmult_comm (/ y)); rewrite Rmult_plus_distr_r;
    rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
      [ rewrite Rmult_1_r | assumption ];
      apply Rplus_le_reg_l with (IZR (up (x / y)) - x / y);
	rewrite Rplus_0_r; unfold Rdiv;
	  replace
	    (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with
	    1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2;
	      exact H2.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
x + (1 - IZR (up (x / y))) * y < Rabs y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  rewrite (Rabs_right _ Hge); apply Rmult_lt_reg_l with (/ y).x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
0 < / y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
/ y * (x + (1 - IZR (up (x / y))) * y) < / y * y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  apply Rinv_0_lt_compat; assumption.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
H1:0 < y
/ y * (x + (1 - IZR (up (x / y))) * y) < / y * y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y));
    rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
      [ rewrite Rmult_1_r | assumption ];
      apply Rplus_lt_reg_l with (IZR (up (x / y)) - 1);
	replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y)));
	  [ idtac | ring ];
	  replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with
	    (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv;
	      intros H2 _; exact H2.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
0 < y
  destruct (total_order_T 0 y) as [[Hlt|Heq]|Hgt].x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Hlt:0 < y
0 < y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Heq:0 = y
0 < y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Hgt:0 > y
0 < y
  assumption.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Heq:0 = y
0 < y
x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Hgt:0 > y
0 < y
  elim H; symmetry ; exact Heq.x, y:R
H:y <> 0
Hge:y >= 0
k0:=(up (x / y) - 1)%Z:Z
H0:IZR (up (x / y)) > x / y /\
IZR (up (x / y)) - x / y <= 1
Hgt:0 > y
0 < y
  apply Rge_le in Hge; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hge Hgt)).
Qed.

Lemma tech8 : forall n i:nat, (n <= S n + i)%nat.forall n i : nat, (n <= S n + i)%nat
Proof.forall n i : nat, (n <= S n + i)%nat
  intros; induction  i as [| i Hreci].n:nat
(n <= S n + 0)%nat
n, i:nat
Hreci:(n <= S n + i)%nat
(n <= S n + S i)%nat
  replace (S n + 0)%nat with (S n); [ apply le_n_Sn | ring ].n, i:nat
Hreci:(n <= S n + i)%nat
(n <= S n + S i)%nat
  replace (S n + S i)%nat with (S (S n + i)).n, i:nat
Hreci:(n <= S n + i)%nat
(n <= S (S n + i))%nat
n, i:nat
Hreci:(n <= S n + i)%nat
S (S n + i) = (S n + S i)%nat
  apply le_S; assumption.n, i:nat
Hreci:(n <= S n + i)%nat
S (S n + i) = (S n + S i)%nat
  apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring.
Qed.