Library Coq.Reals.ArithProp
Require Import Rbase.
Require Import Rbasic_fun.
Require Import Even.
Require Import Div2.
Require Import ArithRing.
Open Local Scope Z_scope.
Open Local Scope R_scope.
Lemma minus_neq_O :
forall n i:nat, (
i <
n)%nat -> (
n -
i)%nat <> 0%nat.
Lemma le_minusni_n :
forall n i:nat, (
i <=
n)%nat -> (
n -
i <=
n)%nat.
Lemma lt_minus_O_lt :
forall m n:nat, (
m <
n)%nat -> (0 <
n -
m)%nat.
Lemma even_odd_cor :
forall n:nat,
exists p :
nat,
n = (2 *
p)%nat \/
n =
S (2 *
p).
Lemma le_double :
forall m n:nat, (2 *
m <= 2 *
n)%nat -> (
m <=
n)%nat.
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).
Lemma tech8 :
forall n i:nat, (
n <=
S n +
i)%nat.