# Library HRwequal

Require Export HRw.

Module mHRwequal (N:Num_w).

Import N.

Module Export HH := mHRw(N).

Definition HRwequal (x y : HRw) : Prop :=

match x with @exist _ _ xx Hxx ⇒

match y with @exist _ _ yy Hyy ⇒

(∀ n, lim n →0 < n → ( (n×|xx + (- yy)|) ≤ w))

end end.

Lemma HRwequal_refl : ∀ x, HRwequal x x.

Proof.

intros x; case x; intros xx Hxx; simpl.

intros.

setoid_replace (xx+ -xx) with 0 by ring.

rewrite abs_pos_val.

setoid_replace (n×0) with 0 by ring.

intros; apply lt_le; apply Aw.

apply le_refl.

Qed.

Lemma HRwequal_sym : ∀ x y, HRwequal x y → HRwequal y x.

Proof.

intros x y; case x; intros xx Hxx; case y; intros yy Hyy; simpl.

intros.

assert (|yy + - xx |==|xx + - yy |).

setoid_replace (yy + -xx) with (- (xx + - yy)) by ring.

rewrite abs_minus; reflexivity.

rewrite H2.

apply H; solve [intuition].

Qed.

Lemma HRwequal_trans : ∀ x y z, HRwequal x y → HRwequal y z → HRwequal x z.

Proof.

intros x; case x; intros xx Hxx;

intros y; case y; intros yy Hyy;

intros z; case z; intros zz Hzz.

simpl; intros Hxy Hyz n Hlim Hlt.

apply le_mult_inv with (a1+a1).

setoid_replace 0 with (0+0) by ring.

apply lt_plus; apply lt_0_1.

apply le_trans with ((1+1)*n*(|xx + - yy| + |yy + - zz|)).

rewrite mult_assoc.

apply le_mult.

setoid_replace 0 with ((1+1)*0) by ring.

apply le_mult.

setoid_replace 0 with (0+0) by ring; apply le_plus; apply lt_le; apply lt_0_1.

apply lt_le; assumption.

setoid_replace (xx + -zz) with ((xx + -yy)+(yy + - zz)) by ring.

apply abs_triang.

ring_simplify.

setoid_replace ((1+1)* w) with (w + w) by ring.

setoid_replace ((1+1)*n) with (n+n) by ring.

apply le_plus.

apply Hxy.

apply ANS2a; assumption.

setoid_replace 0 with (0+0) by ring; apply lt_plus; assumption.

apply Hyz.

apply ANS2a; assumption.

setoid_replace 0 with (0+0) by ring; apply lt_plus; assumption.

Qed.

End mHRwequal.

Module mHRwequal (N:Num_w).

Import N.

Module Export HH := mHRw(N).

Definition HRwequal (x y : HRw) : Prop :=

match x with @exist _ _ xx Hxx ⇒

match y with @exist _ _ yy Hyy ⇒

(∀ n, lim n →0 < n → ( (n×|xx + (- yy)|) ≤ w))

end end.

Lemma HRwequal_refl : ∀ x, HRwequal x x.

Proof.

intros x; case x; intros xx Hxx; simpl.

intros.

setoid_replace (xx+ -xx) with 0 by ring.

rewrite abs_pos_val.

setoid_replace (n×0) with 0 by ring.

intros; apply lt_le; apply Aw.

apply le_refl.

Qed.

Lemma HRwequal_sym : ∀ x y, HRwequal x y → HRwequal y x.

Proof.

intros x y; case x; intros xx Hxx; case y; intros yy Hyy; simpl.

intros.

assert (|yy + - xx |==|xx + - yy |).

setoid_replace (yy + -xx) with (- (xx + - yy)) by ring.

rewrite abs_minus; reflexivity.

rewrite H2.

apply H; solve [intuition].

Qed.

Lemma HRwequal_trans : ∀ x y z, HRwequal x y → HRwequal y z → HRwequal x z.

Proof.

intros x; case x; intros xx Hxx;

intros y; case y; intros yy Hyy;

intros z; case z; intros zz Hzz.

simpl; intros Hxy Hyz n Hlim Hlt.

apply le_mult_inv with (a1+a1).

setoid_replace 0 with (0+0) by ring.

apply lt_plus; apply lt_0_1.

apply le_trans with ((1+1)*n*(|xx + - yy| + |yy + - zz|)).

rewrite mult_assoc.

apply le_mult.

setoid_replace 0 with ((1+1)*0) by ring.

apply le_mult.

setoid_replace 0 with (0+0) by ring; apply le_plus; apply lt_le; apply lt_0_1.

apply lt_le; assumption.

setoid_replace (xx + -zz) with ((xx + -yy)+(yy + - zz)) by ring.

apply abs_triang.

ring_simplify.

setoid_replace ((1+1)* w) with (w + w) by ring.

setoid_replace ((1+1)*n) with (n+n) by ring.

apply le_plus.

apply Hxy.

apply ANS2a; assumption.

setoid_replace 0 with (0+0) by ring; apply lt_plus; assumption.

apply Hyz.

apply ANS2a; assumption.

setoid_replace 0 with (0+0) by ring; apply lt_plus; assumption.

Qed.

End mHRwequal.