Library LUB_spec
LUB specifications
Definition subset := HRw→Prop.
Definition upper_bound (X:subset) (m:HRw) : Prop := ∀ x:HRw, X x → HRwgt m x.
Definition bound_above (X:subset) := ∃ m:HRw, upper_bound X m.
Definition non_empty (X:subset):= {x:HRw| X x}.
Definition upper_bound (X:subset) (m:HRw) : Prop := ∀ x:HRw, X x → HRwgt m x.
Definition bound_above (X:subset) := ∃ m:HRw, upper_bound X m.
Definition non_empty (X:subset):= {x:HRw| X x}.
actually implements the axiom of choice
Parameter nat_like_induction :
∀ P : A → Type,
P a0 →
(∀ n:A, (lim n ∧ 0 ≤ n) → P n → P (plusA n a1)) →
∀ n:A, (lim n ∧ 0≤ n) → P n.
Parameter nat_like_induction_r1 :
∀ H:lim 0 ∧ 0≤0, ∀ P : A → Type,
∀ (h0: P a0),
∀ hr : (∀ n:A, (lim n ∧ 0 ≤ n) → P n → P (plusA n a1)),
nat_like_induction P h0 hr a0 H = h0.
Parameter nat_like_induction_r2 :
∀ P : A → Type,
∀ n:A, ∀ H:lim n∧0≤n,
∀ Hn':lim (n+1)∧0<=(n+1),
∀ (h0: P a0),
∀ hr : (∀ n:A, (lim n ∧ 0 ≤ n) → P n → P (plusA n a1)),
nat_like_induction P h0 hr (n + 1) Hn' =
hr n H (nat_like_induction P h0 hr n H).
Definition power (x:HRw) (n:A) : lim n ∧ 0≤n → HRw.
intros Hn.
apply (nat_like_induction (fun _ ⇒ HRw)) with (n:=n).
exact HRw1.
intros k Hk xk.
apply (HRwmult xk x).
assumption.
Defined.
Parameter power_lim : ∀ x, HRwgt x HRw0 → HRwgt HRw1 x → ∀ a:HRw, HRwgt a HRw0 →
∀ eps:HRw, HRwgt eps HRw0 →
∃ n:A, lim n∧0 ≤n ∧ ∀ H:lim n∧ 0 ≤ n, eps >w (a×w (power x n H)).
Technical lemmas
Notation "2w" := HRw2.
Notation "3w" := HRw3.
Lemma test1 :
(HRw2 ×w HRwinv HRw3 lemma_HRw3) =w ((HRwinv HRw3 lemma_HRw3) +w HRwinv HRw3 lemma_HRw3).
Proof.
intros; unfold HRw2; ring.
Qed.
Lemma test2 : ∀ a b, (HRwinv HRw3 lemma_HRw3 ×w b) +w ((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w a) =w
((HRwinv HRw3 lemma_HRw3) ×w a)+w (HRwinv HRw3 lemma_HRw3 ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a).
intros; unfold HRw2; ring.
Qed.
Lemma HRwgt_one_third : one_third >w HRw0.
Proof.
unfold HRwgt, one_third, HRw3, HRw2, HRw0.
simpl.
∃ (1+1+1+1+1+1).
split.
repeat apply ANS2a;apply ANS1.
split.
setoid_replace 0 with (0+0+0+0+0+0) by ring.
repeat apply lt_plus; apply lt_0_1.
setoid_replace (w × w / (w + w + w) + - 0) with (w × w / (w + w + w)) by ring.
apply le_mult_inv with (x:=w).
apply Aw.
setoid_replace (w × ((1 + 1 + 1 + 1 + 1 + 1) × (w × w / (w + w + w))))
with ((1+1) × ((w+ w + w) × (w × w / (w + w + w)))) by ring.
rewrite div_mod2.
setoid_replace ((1 + 1) × (w × w + - (w × w %% w + w + w))) with ((1+1)* (w× w) + - (1+1)*(w× w %% (w+ w + w))) by ring.
apply le_trans with (w× w + (w × w + - (1+1)*(w+ w+ w))).
pattern (w× w) at 1; setoid_replace (w× w) with ((w× w) +0) by ring.
apply le_plus.
ring_simplify; apply le_refl.
setoid_replace (w × w + 0 + - (1 + 1) × (w + w + w)) with (w × (w + - (1+1+1+1+1+1))) by ring.
setoid_replace 0 with (w × 0) by ring.
apply le_mult.
apply lt_le; apply Aw.
apply le_plus_inv with (1+1+1+1+1+1).
ring_simplify.
apply lt_le; apply lim_lt_w.
split.
repeat( apply ANS2a || apply ANS2b); apply ANS1.
setoid_replace 0 with ((1+1)*(0+ (0+0))) by ring.
apply le_mult.
setoid_replace 0 with (0+0) by ring.
apply le_plus; apply lt_le; apply lt_0_1.
repeat apply le_plus; apply lt_le; apply lt_0_1.
setoid_replace ((1+1) × (w× w)) with (w × w + w× w) by ring.
rewrite plus_assoc.
apply le_plus.
apply le_refl.
apply le_mult_neg.
apply lt_plus_inv with (1+1).
ring_simplify.
setoid_replace 0 with (0+0) by ring.
apply lt_plus; apply lt_0_1.
apply lt_le.
apply div_mod3a.
setoid_replace 0 with (0+0+0) by ring.
repeat apply lt_plus; apply Aw.
left; setoid_replace 0 with (0+0+0) by ring; repeat apply lt_plus; apply Aw.
Qed.
Lemma HRwgt_morphism1 : ∀ x y : HRw, x =w y → ∀ x0 y0 : HRw, x0 =w y0 → (x >w x0 → y >w y0).
Proof.
intros x y Hxy t z Htz;
destruct x as [x Hx]; destruct y as [y Hy]; destruct z as [z Hz]; destruct t as [t Ht]; simpl.
unfold HRwequal in ×.
intros.
destruct H as [n [Hlim [Hn0 Hn]]].
∃ (n+n+n).
assert (H3lim : lim (n+n+n)).
repeat apply ANS2a; assumption.
assert (H3n:0<n+n+n).
setoid_replace 0 with (0+0+0) by ring.
repeat apply lt_plus; assumption.
split.
apply H3lim.
split.
apply H3n.
setoid_replace ((n+n+n)*(y+ -z)) with ((n+n+n)*(y + -x)+ n*(x + -t)+n*(x+ - t) +n*(x + - t) +(n+n+n)*(t + -z)) by ring.
apply le_trans with (oppA w + w + w + w + (oppA w)).
ring_simplify.
apply le_refl.
apply le_plus.
apply le_plus.
apply le_plus.
apply le_plus.
apply abs_new2.
rewrite abs_prod.
rewrite (abs_pos_val (n+n+n)) by (apply lt_le; apply H3n).
setoid_replace (y + - x) with (- (x + - y)) by ring.
rewrite abs_minus.
apply Hxy.
apply H3lim.
apply H3n.
assumption.
assumption.
assumption.
apply abs_new2.
rewrite abs_prod.
rewrite (abs_pos_val (n+n+n)) by (apply lt_le; apply H3n).
apply Htz.
apply H3lim.
apply H3n.
Qed.
Instance HRwgt_morphism : Proper (HRwequal ==> HRwequal ==> Logic.iff) HRwgt.
Proof.
repeat red; split.
apply HRwgt_morphism1; assumption.
apply HRwgt_morphism1; symmetry; assumption.
Qed.
Lemma HRwge_morphism1 : ∀ x y : HRw, x =w y → ∀ x0 y0 : HRw, x0 =w y0 → (x ≥w x0 → y ≥w y0).
Proof.
intros.
generalize (HRwge_prop1 _ _ H1); intros.
apply HRwge_prop2.
intros.
setoid_rewrite <- H.
apply H2.
setoid_rewrite H0.
assumption.
Qed.
Instance HRwge_morphism : Proper (HRwequal ==> HRwequal ==> Logic.iff) HRwge.
repeat red.
intros; split.
apply HRwge_morphism1; assumption.
apply HRwge_morphism1; symmetry; assumption.
Qed.
Lemma R2_4' : ∀ X Y, HRwge X Y → ∀ Z, HRwge (X +w Z) (Y +w Z).
Proof.
intros x y Hxy z.
eapply HRwge_prop2.
generalize (HRwge_prop1 _ _ Hxy).
intros.
generalize (H (c +w -w z)).
intros.
eapply HRwgt_HRwplus_inv_r with (-w z).
rewrite HRwplus_assoc.
rewrite HRwplus_opp.
rewrite HRwplus_comm.
rewrite HRwplus_zero.
apply H1.
eapply HRwgt_HRwplus_inv_r with (z).
rewrite HRwplus_assoc.
rewrite (HRwplus_comm (-w z) z).
rewrite HRwplus_opp.
rewrite (HRwplus_comm c HRw0).
rewrite HRwplus_zero.
assumption.
Qed.
Lemma step_thirds : ∀ a b:HRw, a >w b →
((HRwinv HRw3 lemma_HRw3 ×w b) +w ((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w a)) >w
(((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a)).
Proof.
intros a b Hab.
apply HRwgt_HRwplus_inv_r
with (Z:= -w (((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a))).
ring_simplify; unfold HRwminus.
setoid_replace (-w ((HRwinv HRw3 lemma_HRw3)*w a)) with ((HRwinv HRw3 lemma_HRw3)*w (-w a)) by ring.
setoid_replace (-w (HRwinv HRw3 lemma_HRw3)) with ((HRwinv HRw3 lemma_HRw3)*w (-w HRw1)) by ring.
repeat rewrite HRwmult_assoc.
repeat rewrite <- HRw_distr.
setoid_replace (((-w HRw1) ×w (b ×w HRw2)) +w b) with (-w b) by (unfold HRw2; ring).
rewrite HRwplus_assoc.
setoid_replace ((HRw2×w a)+w (-w a)) with a by (unfold HRw2;ring).
apply R2_5.
split.
apply HRwgt_one_third.
apply HRwgt_HRwplus_inv_l with b.
ring_simplify; assumption.
Qed.
Lemma two_thirds_one_third : ∀ x : HRw, x =w ((two_third ×w x) +w (one_third ×w x)).
Proof.
intros.
setoid_rewrite two_one_third.
setoid_rewrite HRwmult_comm.
setoid_rewrite <- HRw_distr.
setoid_rewrite three_one_third.
ring.
Qed.
Lemma HRw1_3 : ∀ a b , a >w b →
((HRwinv HRw3 lemma_HRw3) ×w a) >w ((HRwinv HRw3 lemma_HRw3) ×w b).
Proof.
intros a b Hab.
eapply HRwgt_HRwplus_inv_r with (-w (one_third ×w b)).
unfold one_third; ring_simplify; unfold HRwminus.
setoid_replace (-w (HRwinv HRw3 lemma_HRw3 ×w b)) with ((HRwinv HRw3 lemma_HRw3) ×w (-w b)) by ring.
rewrite <- HRw_distr.
apply R2_5.
split.
apply HRwgt_one_third.
apply HRwgt_HRwplus_inv_l with b.
ring_simplify; assumption.
Qed.
Notation "3w" := HRw3.
Lemma test1 :
(HRw2 ×w HRwinv HRw3 lemma_HRw3) =w ((HRwinv HRw3 lemma_HRw3) +w HRwinv HRw3 lemma_HRw3).
Proof.
intros; unfold HRw2; ring.
Qed.
Lemma test2 : ∀ a b, (HRwinv HRw3 lemma_HRw3 ×w b) +w ((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w a) =w
((HRwinv HRw3 lemma_HRw3) ×w a)+w (HRwinv HRw3 lemma_HRw3 ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a).
intros; unfold HRw2; ring.
Qed.
Lemma HRwgt_one_third : one_third >w HRw0.
Proof.
unfold HRwgt, one_third, HRw3, HRw2, HRw0.
simpl.
∃ (1+1+1+1+1+1).
split.
repeat apply ANS2a;apply ANS1.
split.
setoid_replace 0 with (0+0+0+0+0+0) by ring.
repeat apply lt_plus; apply lt_0_1.
setoid_replace (w × w / (w + w + w) + - 0) with (w × w / (w + w + w)) by ring.
apply le_mult_inv with (x:=w).
apply Aw.
setoid_replace (w × ((1 + 1 + 1 + 1 + 1 + 1) × (w × w / (w + w + w))))
with ((1+1) × ((w+ w + w) × (w × w / (w + w + w)))) by ring.
rewrite div_mod2.
setoid_replace ((1 + 1) × (w × w + - (w × w %% w + w + w))) with ((1+1)* (w× w) + - (1+1)*(w× w %% (w+ w + w))) by ring.
apply le_trans with (w× w + (w × w + - (1+1)*(w+ w+ w))).
pattern (w× w) at 1; setoid_replace (w× w) with ((w× w) +0) by ring.
apply le_plus.
ring_simplify; apply le_refl.
setoid_replace (w × w + 0 + - (1 + 1) × (w + w + w)) with (w × (w + - (1+1+1+1+1+1))) by ring.
setoid_replace 0 with (w × 0) by ring.
apply le_mult.
apply lt_le; apply Aw.
apply le_plus_inv with (1+1+1+1+1+1).
ring_simplify.
apply lt_le; apply lim_lt_w.
split.
repeat( apply ANS2a || apply ANS2b); apply ANS1.
setoid_replace 0 with ((1+1)*(0+ (0+0))) by ring.
apply le_mult.
setoid_replace 0 with (0+0) by ring.
apply le_plus; apply lt_le; apply lt_0_1.
repeat apply le_plus; apply lt_le; apply lt_0_1.
setoid_replace ((1+1) × (w× w)) with (w × w + w× w) by ring.
rewrite plus_assoc.
apply le_plus.
apply le_refl.
apply le_mult_neg.
apply lt_plus_inv with (1+1).
ring_simplify.
setoid_replace 0 with (0+0) by ring.
apply lt_plus; apply lt_0_1.
apply lt_le.
apply div_mod3a.
setoid_replace 0 with (0+0+0) by ring.
repeat apply lt_plus; apply Aw.
left; setoid_replace 0 with (0+0+0) by ring; repeat apply lt_plus; apply Aw.
Qed.
Lemma HRwgt_morphism1 : ∀ x y : HRw, x =w y → ∀ x0 y0 : HRw, x0 =w y0 → (x >w x0 → y >w y0).
Proof.
intros x y Hxy t z Htz;
destruct x as [x Hx]; destruct y as [y Hy]; destruct z as [z Hz]; destruct t as [t Ht]; simpl.
unfold HRwequal in ×.
intros.
destruct H as [n [Hlim [Hn0 Hn]]].
∃ (n+n+n).
assert (H3lim : lim (n+n+n)).
repeat apply ANS2a; assumption.
assert (H3n:0<n+n+n).
setoid_replace 0 with (0+0+0) by ring.
repeat apply lt_plus; assumption.
split.
apply H3lim.
split.
apply H3n.
setoid_replace ((n+n+n)*(y+ -z)) with ((n+n+n)*(y + -x)+ n*(x + -t)+n*(x+ - t) +n*(x + - t) +(n+n+n)*(t + -z)) by ring.
apply le_trans with (oppA w + w + w + w + (oppA w)).
ring_simplify.
apply le_refl.
apply le_plus.
apply le_plus.
apply le_plus.
apply le_plus.
apply abs_new2.
rewrite abs_prod.
rewrite (abs_pos_val (n+n+n)) by (apply lt_le; apply H3n).
setoid_replace (y + - x) with (- (x + - y)) by ring.
rewrite abs_minus.
apply Hxy.
apply H3lim.
apply H3n.
assumption.
assumption.
assumption.
apply abs_new2.
rewrite abs_prod.
rewrite (abs_pos_val (n+n+n)) by (apply lt_le; apply H3n).
apply Htz.
apply H3lim.
apply H3n.
Qed.
Instance HRwgt_morphism : Proper (HRwequal ==> HRwequal ==> Logic.iff) HRwgt.
Proof.
repeat red; split.
apply HRwgt_morphism1; assumption.
apply HRwgt_morphism1; symmetry; assumption.
Qed.
Lemma HRwge_morphism1 : ∀ x y : HRw, x =w y → ∀ x0 y0 : HRw, x0 =w y0 → (x ≥w x0 → y ≥w y0).
Proof.
intros.
generalize (HRwge_prop1 _ _ H1); intros.
apply HRwge_prop2.
intros.
setoid_rewrite <- H.
apply H2.
setoid_rewrite H0.
assumption.
Qed.
Instance HRwge_morphism : Proper (HRwequal ==> HRwequal ==> Logic.iff) HRwge.
repeat red.
intros; split.
apply HRwge_morphism1; assumption.
apply HRwge_morphism1; symmetry; assumption.
Qed.
Lemma R2_4' : ∀ X Y, HRwge X Y → ∀ Z, HRwge (X +w Z) (Y +w Z).
Proof.
intros x y Hxy z.
eapply HRwge_prop2.
generalize (HRwge_prop1 _ _ Hxy).
intros.
generalize (H (c +w -w z)).
intros.
eapply HRwgt_HRwplus_inv_r with (-w z).
rewrite HRwplus_assoc.
rewrite HRwplus_opp.
rewrite HRwplus_comm.
rewrite HRwplus_zero.
apply H1.
eapply HRwgt_HRwplus_inv_r with (z).
rewrite HRwplus_assoc.
rewrite (HRwplus_comm (-w z) z).
rewrite HRwplus_opp.
rewrite (HRwplus_comm c HRw0).
rewrite HRwplus_zero.
assumption.
Qed.
Lemma step_thirds : ∀ a b:HRw, a >w b →
((HRwinv HRw3 lemma_HRw3 ×w b) +w ((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w a)) >w
(((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a)).
Proof.
intros a b Hab.
apply HRwgt_HRwplus_inv_r
with (Z:= -w (((HRw2 ×w HRwinv HRw3 lemma_HRw3) ×w b) +w (HRwinv HRw3 lemma_HRw3 ×w a))).
ring_simplify; unfold HRwminus.
setoid_replace (-w ((HRwinv HRw3 lemma_HRw3)*w a)) with ((HRwinv HRw3 lemma_HRw3)*w (-w a)) by ring.
setoid_replace (-w (HRwinv HRw3 lemma_HRw3)) with ((HRwinv HRw3 lemma_HRw3)*w (-w HRw1)) by ring.
repeat rewrite HRwmult_assoc.
repeat rewrite <- HRw_distr.
setoid_replace (((-w HRw1) ×w (b ×w HRw2)) +w b) with (-w b) by (unfold HRw2; ring).
rewrite HRwplus_assoc.
setoid_replace ((HRw2×w a)+w (-w a)) with a by (unfold HRw2;ring).
apply R2_5.
split.
apply HRwgt_one_third.
apply HRwgt_HRwplus_inv_l with b.
ring_simplify; assumption.
Qed.
Lemma two_thirds_one_third : ∀ x : HRw, x =w ((two_third ×w x) +w (one_third ×w x)).
Proof.
intros.
setoid_rewrite two_one_third.
setoid_rewrite HRwmult_comm.
setoid_rewrite <- HRw_distr.
setoid_rewrite three_one_third.
ring.
Qed.
Lemma HRw1_3 : ∀ a b , a >w b →
((HRwinv HRw3 lemma_HRw3) ×w a) >w ((HRwinv HRw3 lemma_HRw3) ×w b).
Proof.
intros a b Hab.
eapply HRwgt_HRwplus_inv_r with (-w (one_third ×w b)).
unfold one_third; ring_simplify; unfold HRwminus.
setoid_replace (-w (HRwinv HRw3 lemma_HRw3 ×w b)) with ((HRwinv HRw3 lemma_HRw3) ×w (-w b)) by ring.
rewrite <- HRw_distr.
apply R2_5.
split.
apply HRwgt_one_third.
apply HRwgt_HRwplus_inv_l with b.
ring_simplify; assumption.
Qed.
properties of power
Lemma power_0 : ∀ a, ∀ H0: lim 0 ∧ 0≤ 0, (power a 0 H0) =w HRw1.
Proof.
intros a H0.
unfold power.
rewrite nat_like_induction_r1.
reflexivity.
Qed.
Lemma power_n1 : ∀ a, ∀ n, ∀ Hn:lim n ∧ 0≤n, ∀ Hn1: lim (n+1)∧ 0≤ (n+1),
power a (n+1) Hn1 =w power a n Hn ×w a.
Proof.
intros a n Hn Hn1.
unfold power at 1.
rewrite nat_like_induction_r2 with (H:=Hn).
unfold power.
reflexivity.
Qed.
Lemma HRwgt_HRwmult : ∀ a b c, a>w HRw0 → b >w c → (a ×w b) >w (a×w c).
Proof.
intros.
apply HRwgt_HRwplus_inv_r with (-w (a×w c)).
setoid_replace (((a ×w c) +w (-w (a ×w c)))) with HRw0 by ring.
setoid_replace ((a×w b) +w (-w (a ×w c))) with (a×w(b +w -w c)) by ring.
apply R2_5.
split.
assumption.
apply HRwgt_HRwplus_inv_r with c.
ring_simplify.
assumption.
Qed.
Lemma power_HRwgt : ∀ a, a >w HRw0 → ∀ n, ∀ H:(lim n ∧0≤n), power a n H >w HRw0.
Proof.
intros a Ha n Hn.
apply (nat_like_induction (fun (x:A) ⇒ ∀ Hx: lim x ∧ 0≤x, power a x Hx >w HRw0)).
intros; rewrite power_0.
∃ 1.
split.
apply ANS1.
split.
apply lt_0_1.
ring_simplify.
apply le_refl.
intros.
rewrite power_n1 with (Hn:=H).
setoid_replace HRw0 with (a×w HRw0) by ring.
rewrite <- (HRwmult_comm a).
apply HRwgt_HRwmult.
assumption.
eapply H0.
apply Hn.
Qed.
Lemma lt_power_Sn_n : ∀ a, ∀ n, ∀ Hn:lim n ∧ 0≤n, ∀ Hn1: lim (n+1)∧ 0≤ (n+1),
a >w HRw0 → HRw1 >w a → (power a n Hn) >w (power a (n+1) Hn1).
Proof.
intros.
rewrite power_n1 with (Hn:=Hn).
setoid_replace (power a n Hn) with ((power a n Hn)*w HRw1) at 1 by ring.
apply HRwgt_HRwmult.
apply power_HRwgt.
assumption.
assumption.
Qed.
End lub_spec.
Proof.
intros a H0.
unfold power.
rewrite nat_like_induction_r1.
reflexivity.
Qed.
Lemma power_n1 : ∀ a, ∀ n, ∀ Hn:lim n ∧ 0≤n, ∀ Hn1: lim (n+1)∧ 0≤ (n+1),
power a (n+1) Hn1 =w power a n Hn ×w a.
Proof.
intros a n Hn Hn1.
unfold power at 1.
rewrite nat_like_induction_r2 with (H:=Hn).
unfold power.
reflexivity.
Qed.
Lemma HRwgt_HRwmult : ∀ a b c, a>w HRw0 → b >w c → (a ×w b) >w (a×w c).
Proof.
intros.
apply HRwgt_HRwplus_inv_r with (-w (a×w c)).
setoid_replace (((a ×w c) +w (-w (a ×w c)))) with HRw0 by ring.
setoid_replace ((a×w b) +w (-w (a ×w c))) with (a×w(b +w -w c)) by ring.
apply R2_5.
split.
assumption.
apply HRwgt_HRwplus_inv_r with c.
ring_simplify.
assumption.
Qed.
Lemma power_HRwgt : ∀ a, a >w HRw0 → ∀ n, ∀ H:(lim n ∧0≤n), power a n H >w HRw0.
Proof.
intros a Ha n Hn.
apply (nat_like_induction (fun (x:A) ⇒ ∀ Hx: lim x ∧ 0≤x, power a x Hx >w HRw0)).
intros; rewrite power_0.
∃ 1.
split.
apply ANS1.
split.
apply lt_0_1.
ring_simplify.
apply le_refl.
intros.
rewrite power_n1 with (Hn:=H).
setoid_replace HRw0 with (a×w HRw0) by ring.
rewrite <- (HRwmult_comm a).
apply HRwgt_HRwmult.
assumption.
eapply H0.
apply Hn.
Qed.
Lemma lt_power_Sn_n : ∀ a, ∀ n, ∀ Hn:lim n ∧ 0≤n, ∀ Hn1: lim (n+1)∧ 0≤ (n+1),
a >w HRw0 → HRw1 >w a → (power a n Hn) >w (power a (n+1) Hn1).
Proof.
intros.
rewrite power_n1 with (Hn:=Hn).
setoid_replace (power a n Hn) with ((power a n Hn)*w HRw1) at 1 by ring.
apply HRwgt_HRwmult.
apply power_HRwgt.
assumption.
assumption.
Qed.
End lub_spec.