Library LaugwitzSchmieden

Require Export Arith. Require Export Ltac.
Require Export Numbers_facts.

Lemma Zmult_lt_reg_l: n m p : Z, (0 < p)%Z (p × n < p × m)%Z (n < m)%Z.
Proof.
intros.
rewrite (Zmult_comm p n) in ×.
rewrite (Zmult_comm p m) in ×.
eapply Zmult_lt_reg_r; eassumption.
Qed.

Laugwitz-Schmieden

Module LS <: Num_facts.

Definition A :=natZ.

Operations

Definition a0 : A := fun (n:nat) ⇒ 0%Z.
Definition a1: A := fun (n:nat) ⇒ 1%Z.

Definition plusA (u v:A) : A := fun (n:nat) ⇒ Zplus (u n) (v n).
Definition oppA (u:A) : A := fun (n:nat) ⇒ Zopp (u n).

Definition minusA x y := plusA x (oppA y).

Definition multA (u v:A) : A := fun (n:nat) ⇒ Zmult (u n) (v n).

Definition divA (u v:A) : A := fun (n:nat) ⇒ Z.div (u n) (v n).
Definition modA (u v:A) : A := fun (n:nat) ⇒ Z.modulo (u n) (v n).

Definition absA (u:A) : A := fun (n:nat) ⇒ Z.abs (u n).

Notation "x + y " := (plusA x y).
Notation "x * y " := (multA x y).
Notation "x / y " := (divA x y).
Notation "x mod% y" := (modA x y) (at level 60).
Notation "0" := (a0).
Notation "1" := (a1).
Notation "- x" := (oppA x).
Notation "| x |" := (absA x) (at level 60).

Relations
Definition equalA (u v:A) :=
    N:nat, n:nat, n>N (u n)=(v n).

Notation "x =A y" := (equalA x y) (at level 80).

Definition leA (u v:A) :=
    N:nat, n:nat, n>N Zle (u n) (v n).

Definition ltA (u v:A) :=
    N:nat, n:nat, n>N Zlt (u n) (v n).

Notation "x <=A y" := (leA x y) (at level 50).
Notation "x <A y" := (ltA x y) (at level 50).

Definition std (u:A) := N:nat, n m, n>N m>N (u n)=(u m).

Definition non_std (u:A) := ¬std u.

Definition lim (a:A) := p, std p leA a0 p ltA (absA a) p.

Tactics

Ltac gen_eq n0 := (match goal with |[ H : n:nat, n > ?X _ |- _ ] ⇒
   let myH:=fresh "Hyp" in assert (myH:(n0 > X)) by (unfold sum_plus1 in *;omega); generalize (H n0 myH); clear H; intro end).

Ltac gen_props :=
match goal with
  [|- n:nat, _ ] ⇒ let id:= fresh "p" in let Hid := fresh "Hp" in (intros id Hid; repeat (gen_eq id))
| [|- False] ⇒ let l:= collect_nats in repeat (gen_eq (sum_plus1 l))
end .

Ltac unfold_intros := unfold lim, std, leA, ltA, equalA, absA, minusA, multA, plusA, divA, modA, oppA, A, a0, a1; intros.

Ltac solve_ls_w_l x :=
unfold_intros;
destruct_exists;
let l:= collect_nats in (sum_plus1 l); simpl;
gen_props;
(apply x|| eapply x); solve [eassumption | omega].

Ltac autorew_aux :=
match goal with [H:(_=_)%Z |- _ ] ⇒ rewrite <- H end.

Ltac autorew := repeat autorew_aux.

Ltac solve_ls :=
(unfold_intros;
solve [ intros; solve [omega | ring] |
destruct_exists; try gen_props; intros; omega |
destruct_exists; let l:= collect_nats in (sum_plus1 l); intros; ring |
destruct_exists; let l:= collect_nats in (sum_plus1 l); simpl; gen_props; autorew; solve [assumption | omega | ring]]).


Lemma equalA_refl : x, x =A x.
Proof.
solve_ls.
Qed.

Lemma equalA_sym : x y, x =A y y =A x.
Proof.
solve_ls.
Qed.

Lemma equalA_trans : x y z, x =A y y =A z x=A z.
Proof.
solve_ls.
Qed.

Instance equalA_equiv : Equivalence equalA.
Proof.
split; red; [apply equalA_refl | apply equalA_sym | apply equalA_trans ].
Qed.

Morphisms

Instance plusA_morphism : Proper (equalA ==> equalA ==> equalA) plusA.
Proof.
repeat red; solve_ls.
Qed.

Instance oppA_morphism : Proper (equalA ==> equalA) oppA.
Proof.
repeat red; solve_ls.
Qed.

Instance multA_morphism : Proper (equalA ==> equalA ==> equalA) multA.
Proof.
repeat red; solve_ls.
Qed.

Instance absA_morphism : Proper (equalA ==> equalA) absA.
Proof.
repeat red; solve_ls.
Qed.

Instance leA_morphism : Proper (equalA ==> equalA ==> Logic.iff) leA.
Proof.
repeat red; unfold_intros; split; solve_ls.
Qed.

Instance ltA_morphism : Proper (equalA ==> equalA ==> Logic.iff) ltA.
Proof.
repeat red; unfold_intros; split; solve_ls.
Qed.

Instance divA_morphism : Proper (equalA ==> equalA ==> equalA) divA.
Proof.
repeat red; solve_ls.
Qed.

Instance modA_morphism : Proper (equalA ==> equalA ==> equalA) modA.
Proof.
repeat red; unfold_intros; solve_ls.
Qed.

Implementation of axioms of Numbers.v and Numbers_facts.v
Ring properties

Lemma plus_neutral : x:A,0 + x =A x.
Proof.
solve_ls.
Qed.

Lemma plus_comm : x y, x + y =A y + x.
Proof.
solve_ls.
Qed.

Lemma plus_assoc : x y z, x + (y + z) =A (x + y) + z.
Proof.
solve_ls.
Qed.

Lemma plus_opp : x:A, x + (- x) =A a0.
Proof.
solve_ls.
Qed.

Lemma mult_neutral : x, a1 × x =A x.
Proof.
solve_ls.
Qed.

Lemma mult_comm : x y, x × y =A y × x.
Proof.
solve_ls.
Qed.

Lemma mult_assoc : x y z, x × (y × z) =A (x × y) × z.
Proof.
solve_ls.
Qed.

Lemma mult_absorb : x, x × a0 =A a0.
Proof.
solve_ls.
Qed.

Lemma mult_distr_l : x y z, (x+y)*z =A x×z + y×z.
Proof.
solve_ls.
Qed.

Definition Radd_0_l := plus_neutral.
Definition Radd_comm := plus_comm.
Definition Radd_assoc :=plus_assoc.
Definition Rmul_1_l :=mult_neutral.
Definition Rmul_comm :=mult_comm.
Definition Rmul_assoc := mult_assoc.
Definition Rdistr_l := mult_distr_l.

Lemma Rsub_def : x y : A, (minusA x y) =A (plusA x (oppA y)).
Proof.
intros; unfold minusA; apply equalA_refl.
Qed.

Definition Ropp_def := plus_opp.

Lemma stdlib_ring_theory : ring_theory a0 a1 plusA multA minusA oppA equalA.
Proof.
constructor.
exact Radd_0_l.
exact Radd_comm.
exact Radd_assoc.
exact Rmul_1_l.
exact Rmul_comm.
exact Rmul_assoc.
exact Rdistr_l.
exact Rsub_def.
exact Ropp_def.
Qed.

Add Ring A_ring : stdlib_ring_theory (abstract).

Lemma mult_distr_r : x y z, x*(y+z) =A x×y + x×z.
Proof.
intros; ring.
Qed.

absA

Lemma abs_pos : x, a0 A |x|.
Proof.
unfold_intros.
0%nat.
intros; simpl.
assert ((x n)<>0x n=0)%Z by omega.
destruct H0.
assert (0 < Z.abs (x n))%Z by (apply Z.abs_pos; assumption).
omega.
rewrite H0; simpl; omega.
Qed.

Lemma abs_pos_val : x, a0A x |x|=A x.
Proof.
solve_ls_w_l Z.abs_eq.
Qed.

Lemma abs_neg_val : x, xA a0 |x|=A -x.
Proof.
solve_ls_w_l Z.abs_neq.
Qed.

Lemma abs_new : x a, xA a -x A a |x|A a.
Proof.
unfold_intros; destruct_exists.
let l := collect_nats in (sum_plus1 l).
gen_props.
assert (Hom:(x p<0)%Z(x p0)%Z)by omega.
elim Hom; clear Hom; intros Hom'.
rewrite Z.abs_neq.
assumption.
omega.
rewrite Z.abs_eq.
assumption.
omega.
Qed.

Lemma abs_new2 : x a, |x|A a -a A x .
Proof.
unfold_intros; destruct_exists.
let l := collect_nats in (sum_plus1 l).
gen_props.
assert (Hom:(x p<0)%Z(x p0)%Z)by omega.
elim Hom; clear Hom; intros Hom'.
rewrite Z.abs_neq in ×.
omega.
omega.
rewrite Z.abs_eq in ×.
omega.
omega.
Qed.

Lemma abs_triang : x y, |x+y| A |x| + | y |.
Proof.
solve_ls_w_l Z.abs_triangle.
Qed.

Lemma abs_prod : x y, |x × y| =A |x| × |y|.
Proof.
solve_ls_w_l Z.abs_mul.
Qed.

Lemma div_mod : a b, 0<A aa<A 0 b =A a*(b / a) + (b mod% a).
Proof.
intros; destruct H.
revert a b H.
solve_ls_w_l Z_div_mod_eq_full.
revert a b H.
solve_ls_w_l Z_div_mod_eq_full.
Qed.

Lemma div_mod2 : a b, 0<A aa<A 0 a*(b/a) =A b + - (b mod% a).
Proof.
intros a b H; generalize (div_mod a b H).
revert a b H.
solve_ls.
Qed.

Lemma div_mod3a : a b, 0 <A a (b mod% a) <A a.
Proof.
solve_ls_w_l Z_mod_lt.
Qed.

Lemma div_mod3b : a b, 0 <A a 0 A (b mod% a).
Proof.
solve_ls_w_l Z_mod_lt.
Qed.

Lemma div_mod3 : a b, 0<A a |(b mod% a)| <A a.
Proof.
intros.
rewrite abs_pos_val.
apply div_mod3a.
assumption.
apply div_mod3b.
assumption.
Qed.

Lemma lt_le : x y, (x <A y) (x A y).
Proof.
solve_ls.
Qed.

Lemma div_mod3_abs: a b:A, 0<A b b<A 0 | a mod% b | A |b|.
Proof.
intros; destruct H.
rewrite (abs_pos_val b).
apply lt_le; apply div_mod3.
assumption.
apply lt_le; assumption.
revert a b H.
unfold_intros.
destruct H; destruct_exists.
(x+1)%nat.
gen_props.
rewrite (Z.abs_neq (b p)).
generalize (Z_mod_neg (a p) (b p) H); intros H'; destruct H'.
rewrite Z.abs_neq.
omega.
assumption.
omega.
Qed.

Lemma div_le : a b c, 0 <A c a A b a / c A b / c.
Proof.
solve_ls_w_l Z_div_le.
Qed.

Lemma div_pos : a b, 0 A a 0 <A b 0 A a/b.
Proof.
solve_ls_w_l Z_div_pos.
Qed.

Lemma bingo : x y:Z, (x<y xy)%Z.
Proof.
unfold_intros.
omega.
Qed.

Lemma bingo2 : x y:Z, (x>y xy)%Z.
Proof.
unfold_intros.
omega.
Qed.

Lemma div_idg : x y, a0 <A y (x × y) / y =A x.
Proof.
unfold_intros.
destruct_exists.
let l:=collect_nats in (sum_plus1 l).
gen_props.
apply Z_div_mult_full.
apply bingo2.
omega.
Qed.

Lemma mult_le : a b c d,
   a0 A a a A b a0 A c c A d a×c A b × d.
Proof.
solve_ls_w_l Zmult_le_compat.
Qed.

Lemma le_refl : x, x A x.
Proof.
solve_ls.
Qed.

Lemma le_trans : x y z, x A y y A z x A z .
Proof.
solve_ls.
Qed.

Lemma lt_plus : x y z t, x <A y z <A t (x + z) <A (y + t).
Proof.
solve_ls.
Qed.

Lemma mult_pos : x y : A, 0<A x 0<A y 0<A x×y.
Proof.
solve_ls_w_l Z.mul_pos_pos.
Qed.

Lemma lt_plus_inv : x y z, (x + z) <A (y + z) x <A y .
Proof.
solve_ls.
Qed.

Lemma le_plus : x y z t, x A y z A t (x + z) A (y + t).
Proof.
solve_ls.
Qed.

Lemma le_lt_plus : x y z t, x A y z <A t (x + z) <A (y + t).
Proof.
solve_ls.
Qed.

Lemma le_plus_inv : x y z, (x + z) A (y + z) x A y .
Proof.
solve_ls.
Qed.

Lemma le_mult_simpl : x y z , (a0 A z) (x A y)-> (x × z) A (y ×z).
Proof.
solve_ls_w_l Zmult_le_compat_r.
Qed.

Lemma le_mult : x y z, a0 A x y A z x×y A x×z.
Proof.
solve_ls_w_l Zmult_le_compat_l.
Qed.

Lemma lt_mult_inv : x y z, a0 <A x (x × y) <A (x × z) y <A z .
Proof.
solve_ls_w_l Zmult_lt_reg_l.
Qed.

Lemma Zlt_mult_inv2 : x y z:Z, (x < 0 (x × y) < (x × z) z < y)%Z .
Proof.
intros.
apply Zmult_lt_reg_l with (- x)%Z.
omega.
apply Zplus_lt_reg_l with (x× z + x×y)%Z.
ring_simplify.
assumption.
Qed.

Lemma lt_mult_inv2 : x y z, x <A 0 (x × y) <A (x × z) z <A y .
Proof.
solve_ls_w_l Zlt_mult_inv2.
Qed.

Lemma Zle_mult_inv2 : x y z:Z, (x < 0 (x × y) (x × z) z y)%Z.
Proof.
intros.
apply Zmult_le_reg_r with (-x)%Z.
omega.
ring_simplify.
eapply Zplus_le_reg_l with (x×y + z×x)%Z.
ring_simplify.
apply H0.
Qed.

Lemma le_mult_inv2 : x y z, x <A 0 (x × y) A (x × z) z A y .
Proof.
solve_ls_w_l Zle_mult_inv2.
Qed.

Lemma lt_mult : x y z, 0 <A x y <A z x×y <A x×z.
Proof.
solve_ls_w_l Zmult_lt_compat_l.
Qed.

Lemma Zle_mult_inv : x y z:Z, (0 < x)%Z (x × y x × z)%Z (y z)%Z.
Proof.
intros.
eapply Zmult_lt_0_le_reg_r.
eassumption.
rewrite (Zmult_comm y x).
rewrite (Zmult_comm z x).
eassumption.
Qed.

Lemma le_mult_inv : x y z, a0 <A x (x × y) A (x × z) y A z .
Proof.
solve_ls_w_l Zle_mult_inv.
Qed.

Lemma le_mult_general :
   x y z t, 0 A x x A y 0 A z z A t x×z A y×t.
Proof.
solve_ls_w_l Zmult_le_compat.
Qed.

Lemma le_mult_neg : x y z, x <A 0 y A z x×z A x×y.
Proof.
solve_ls_w_l Z.mul_le_mono_neg_l.
Qed.

Lemma lt_0_1 : (a0 <A a1).
Proof.
solve_ls.
Qed.

Lemma lt_m1_0 : (-a1 <A 0).
Proof.
solve_ls.
Qed.

Lemma lt_trans : x y z, x <A y y <A z x <A z .
Proof.
solve_ls.
Qed.

Lemma le_lt_trans : x y z, x A y y <A z x <A z .
Proof.
solve_ls.
Qed.

Lemma lt_le_trans : x y z, x <A y y A z x <A z .
Proof.
solve_ls.
Qed.

Lemma lt_le_2 : x y, (x <A y) (x+1 A y).
Proof.
solve_ls.
Qed.

Lemma Znot_le_lt : x y:Z, ¬(x y)%Z (y < x)%Z.
Proof.
intros; omega.
Qed.

Lemma abs_minus : x, | - x| =A |x|.
Proof.
solve_ls_w_l Z.abs_opp.
Qed.

Lemma abs_max : x, x A |x|.
Proof.
unfold_intros.
destruct_exists.
0%nat.
intros.
rewrite Z.abs_max.
assert (H':((x n)<= -(x n) (x n) - (x n))%Z) by omega.
destruct H'.
rewrite Zmax_right.
omega.
omega.
rewrite Zmax_left.
omega.
omega.
Qed.

Lemma le_id : x y, x A y y A x x =A y.
Proof.
solve_ls.
Qed.

Lemma not_lt_0_0 : ¬a0 <A a0.
Proof.
unfold_intros.
intro H; destruct H.
assert (0<0)%Z.
apply (H (x+1)%nat).
omega.
omega.
Qed.

Lemma contradict_lt_le : s x, s <A x x A s False.
Proof.
solve_ls.
Qed.

Lemma le_lt_False : x y, x A y y <A x False.
Proof.
solve_ls.
Qed.

Lemma div_le2 : a b, 0 <A a 0A b a*(b/a) A b.
Proof.
intros.
rewrite div_mod2.
setoid_replace b with (b+0) at 3 by ring.
apply le_plus.
apply le_refl.
apply le_plus_inv with (b mod%a).
ring_simplify.
apply div_mod3b.
assumption.
left.
assumption.
Qed.

properties of lim

Lemma ANS1 : lim a1.
Proof.
unfold lim.
(fun (n:nat) ⇒ 2%Z).
split.
unfold std.
0%nat.
intros; trivial.
split.
unfold leA, ltA, a0; simpl.
0%nat.
intros; solve [auto with zarith].
rewrite abs_pos_val.
unfold ltA, a1; intros.
0%nat.
intros; simpl; omega.
unfold leA; intros.
0%nat.
unfold a0, a1.
intros; simpl; omega.
Qed.

Lemma ANS2a : x y, lim x lim y lim (x + y).
Proof.
intros x y Hx Hy.
elim Hx.
intros pp (Hstdpp, (Hle0pp,Habspp)).
elim Hy.
intros qq (Hstdqq, (Hle0qq,Habsqq)).
unfold lim.

unfold absA,ltA,a0 in ×.
elim Habspp.
intros a Ha.
elim Habsqq.
intros b Hb.

elim Hle0pp.
intros r Hr.
elim Hle0qq.
intros s Hs.

elim Hstdpp.
intros ep Hep.
elim Hstdqq.
intros eq Heq.

(fun (n:nat) ⇒ (Zplus (pp (a+r+ep+1)%nat) (qq (b+s+eq+1)%nat))).
split.
unfold std.
(0)%nat.
intros; trivial.
split.
unfold leA, a0.
(plus a (plus b (plus r s)))%nat.
intros.
assert (Zle 0 (pp (a+r+ep+1)%nat)).
apply Hr.
omega.
assert (Zle 0 (qq (b+s+eq+1)%nat)).
apply Hs.
omega.
omega.
unfold plusA.
(plus ep (plus eq (plus a b)))%nat.
intros.

apply Zle_lt_trans with (m:=Zplus (Zabs (x n)) (Zabs (y n))).
apply Zabs_triangle.
assert ( a b c d:Z, Zlt a b Zlt c d Zlt (Zplus a c) (Zplus b d)).
intros; omega.
apply H0.
replace (pp (a + r + ep + 1)%nat) with (pp n).
apply Ha.
omega.
apply Hep.
omega.
omega.
replace (qq (b + s + eq + 1)%nat) with (qq n).
apply Hb.
omega.
apply Heq.
omega.
omega.
Qed.

Lemma ANS2b : x y, lim x lim y lim (x × y).
Proof.
intros x y Hx Hy.
elim Hx.
intros pp (Hstdpp, (Hle0pp,Habspp)).
elim Hy.
intros qq (Hstdqq, (Hle0qq,Habsqq)).
unfold lim.

unfold absA,ltA,a0 in ×.
elim Habspp.
intros a Ha.
elim Habsqq.
intros b Hb.

elim Hle0pp.
intros r Hr.
elim Hle0qq.
intros s Hs.

elim Hstdpp.
intros ep Hep.
elim Hstdqq.
intros eq Heq.

(fun (n:nat) ⇒ (Zmult (Zabs (pp (a+r+ep+1)%nat)+1%Z) (Zabs (qq (b+s+eq+1)%nat)+1%Z))).
split.
unfold std.
(0)%nat.
intros; trivial.
split.
unfold leA, a0.
(plus a (plus b (plus r s)))%nat.
intros.
solve [auto with zarith].

unfold multA.
(plus ep (plus eq (plus a b)))%nat.
intros.
rewrite Zabs_Zmult.
apply Zmult_lt_compat.
split.
solve [auto with zarith].
rewrite (Zabs_eq (pp (a + r + ep + 1)%nat)).
apply Zlt_le_trans with (m:= pp (a + r + ep + 1)%nat ).
replace (pp (a + r + ep + 1)%nat) with (pp n).
apply Ha.
omega.
apply Hep.
omega.
omega.
omega.
apply Hr.
omega.
split.
solve [auto with zarith].
rewrite (Zabs_eq (qq (b + s + eq + 1)%nat)).
apply Zlt_le_trans with (m:= qq (b + s + eq + 1)%nat ).
replace (qq (b + s + eq + 1)%nat) with (qq n).
apply Hb.
omega.
apply Heq.
omega.
omega.
omega.
apply Hs.
omega.
Qed.

Lemma ANS4 : x, ( y, lim y | x | A | y |)-> lim x.
Proof.
intros.
elim H; clear H.
intros y (Hlimy,Hy).
unfold lim in ×.
elim Hlimy.
intros n (Hstdn, (Hle0n,Hyn)).
n.
split.
solve [auto].
split.
solve [auto].
apply le_lt_trans with (y:=(|y|)); assumption.
Qed.

Definition std_alt (u:A) := N:nat, a, n:nat, n > N u n = a.

Lemma std_std_alt : u:A, std u std_alt u.
Proof.
intros u; split.
intros H ; unfold std, std_alt in ×.
destruct H as [N HN].
N.
(u (plus N 1)).
intros.
apply HN.
easy.
omega.
intros H; unfold std, std_alt in ×.
destruct H as [N HN].
N.
intros.
destruct HN as [a Ha].
apply eq_trans with a.
now apply Ha.
now (symmetry; apply Ha).
Qed.

Lemma std_A0_dec : x, std x x <A 0\/(x =A 0)\/0 <A x.
Proof.
intros x H.
assert (H':std_alt x) by now apply std_std_alt.
clear H.
destruct H' as [N [a Ha]].
assert (Hdec:(a<0%Za=0%Za>0%Z)%Z) by omega.
destruct Hdec as [HH | [ HH| HH ]].
left.
N.
intros; unfold a0.
now rewrite Ha.
right; left.
N.
now subst.
right; right.
N.
intros; unfold a0.
rewrite Ha.
omega.
easy.
Qed.

Lemma std_lim : x, std x lim x.
Proof.
intros x Hstdx.
unfold lim, std in ×.
elim Hstdx.
intros N HN.
(fun (n:nat) ⇒ (Zabs (x (N+1)%nat)+1)%Z).
split.
0%nat; intros; trivial.
split.
unfold leA.
0%nat; intros; simpl.
unfold a0.
solve [auto with zarith].
unfold ltA.
N.
intros.
unfold absA.
rewrite (HN (N+1)%nat n).
solve [auto with zarith].
solve [auto with zarith].
assumption.
Qed.

Instance lim_morphism : Proper (equalA ==> Logic.iff) lim.
repeat red.
unfold_intros.
split.

unfold_intros; destruct_exists.
destruct H1 as [H1' [H2' H3']].
H0.
split.
assumption.
split.
assumption.
elim H3'.
intros x0 Hx0.
(H+x0+1)%nat.
intros.
rewrite <- H2.
apply Hx0.
omega.
omega.

unfold_intros; destruct_exists.
destruct H1 as [H1' [H2' H3']].
H0.
split.
assumption.
split.
assumption.
elim H3'.
intros x0 Hx0.
(H+x0+1)%nat.
intros.
rewrite H2.
apply Hx0.
omega.
omega.
Qed.

beta may be w or some non-standard Laugwitz-Schmieden number which is <= w
Definition beta : A := fun (n:nat) ⇒ (Z_of_nat n).

Lemma Abeta : 0 <A beta.
Proof.
unfold ltA,a0,beta.
1%nat.
intros.
omega.
Qed.

Lemma beta_std : ¬std beta.
Proof.
intro H; unfold std in ×.
elim H; clear H; intros N HN.
unfold beta in ×.
assert (H1:(S N>N)%nat).
omega.
assert (H2:(S (S N)>N)%nat).
omega.
generalize (HN (S N)%nat (S(S N))%nat H1 H2); intro Heq.
assert (S N=S (S N)).
apply inj_eq_rev; assumption.
injection H; intros Hinj.
assert (Hth:( n:nat, ¬n=(S n))).
intros n; elim n.
simpl; discriminate.
intros n0 Hn0 H'.
apply Hn0.
injection H'.
solve [auto].
generalize (Hth N); intros HthN.
solve [auto].
Qed.

Lemma beta_lim : ¬ lim beta.
Proof.
intro H; unfold lim in ×.
elim H; clear H; intros p (Hstdp,(Hle0p,Hwp)).
unfold ltA,a0 in ×.
elim Hstdp.
intros b Hb.
elim Hwp.
intros a Ha.
elim Hle0p.
intros c Hc.
pose (px:=p (a+b+c+1)%nat).
assert (0 px)%Z.
apply Hc.
omega.
pose (x:=((Zabs_nat px)+a+b+c+1)%nat).
assert ((|beta |) (x) < p (x))%Z.
apply Ha.
unfold px,x in ×.
omega.

assert ((|beta |) (x) p (x))%Z.
unfold absA in ×.
unfold beta.
unfold x.
replace (p (Zabs_nat px + a + b + c + 1)%nat)%Z with
(p (a+b+c+1)%nat)%Z.
rewrite Zabs_eq.
replace (Zabs_nat px + a + b + c + 1)%nat with (Zabs_nat (px + (Z_of_nat (a + b + c + 1))))%nat.
rewrite inj_Zabs_nat.
rewrite Zabs_eq.
unfold px.
omega.
omega.
rewrite Zabs_nat_Zplus.
rewrite Zabs_nat_Z_of_nat.
ring.
unfold px; apply Hc.
omega.
solve [auto with zarith].
solve [auto with zarith].
apply Hb.
omega.
omega.
omega.
Qed.

Lemma nat_Z : a:Z, (0 a)%Z qnat, Z.of_nat qnat = a.
Proof.
intros.
(Z.to_nat a).
apply Z2Nat.id; assumption.
Qed.

Lemma std_alt_lt_beta : a, std_alt a 0A a a <A beta.
Proof.
intros.
destruct H as [Hn Hp].
destruct Hn as [n Hn].
destruct Hn as [q Hq].
destruct Hp as [p Hp].
unfold beta, ltA.
assert (Hq0: (0q)%Z).
generalize (Hq (n+p+1)%nat); intros.
generalize (Hp (n+p+1)%nat); intros.
rewrite <- H.
apply H0.
omega.
omega.
elim (nat_Z q Hq0).
intros qnat Hqnat.
(n+qnat+p)%nat.
intros;rewrite Hq by omega.
rewrite <- Hqnat.
omega.
Qed.

Lemma lim_lt_beta : a, lim a 0A a a <A beta.
Proof.
unfold lim;intros.
destruct H as [[c H] H1].
destruct H as [Hex [Hex2 Hex3]].
assert (std_alt c) by (apply std_std_alt; assumption).
rewrite abs_pos_val in Hex3 by assumption.
apply lt_trans with c.
assumption.
apply std_alt_lt_beta; split; assumption.
Qed.

End LS.