Let a, b, c and d be given.
Assume HaR HbR HcR HdR.
Assume Ha0 Hb0 Hc0 Hd0.
We prove the intermediate
claim Hexab:
∃r : set, r ∈ R ∧ Rlt 0 r ∧ Rlt r a ∧ Rlt r b.
Apply Hexab to the current goal.
Let r12 be given.
Assume Hr12.
We prove the intermediate
claim Hr12b:
Rlt r12 b.
An
exact proof term for the current goal is
(andER ((r12 ∈ R ∧ Rlt 0 r12) ∧ Rlt r12 a) (Rlt r12 b) Hr12).
We prove the intermediate
claim Hr12left:
(r12 ∈ R ∧ Rlt 0 r12) ∧ Rlt r12 a.
An
exact proof term for the current goal is
(andEL ((r12 ∈ R ∧ Rlt 0 r12) ∧ Rlt r12 a) (Rlt r12 b) Hr12).
We prove the intermediate
claim Hr12a:
Rlt r12 a.
An
exact proof term for the current goal is
(andER (r12 ∈ R ∧ Rlt 0 r12) (Rlt r12 a) Hr12left).
We prove the intermediate
claim Hr12pair:
r12 ∈ R ∧ Rlt 0 r12.
An
exact proof term for the current goal is
(andEL (r12 ∈ R ∧ Rlt 0 r12) (Rlt r12 a) Hr12left).
We prove the intermediate
claim Hr12R:
r12 ∈ R.
An
exact proof term for the current goal is
(andEL (r12 ∈ R) (Rlt 0 r12) Hr12pair).
We prove the intermediate
claim Hr12pos:
Rlt 0 r12.
An
exact proof term for the current goal is
(andER (r12 ∈ R) (Rlt 0 r12) Hr12pair).
We prove the intermediate
claim Hexcd:
∃r : set, r ∈ R ∧ Rlt 0 r ∧ Rlt r c ∧ Rlt r d.
Apply Hexcd to the current goal.
Let r34 be given.
Assume Hr34.
We prove the intermediate
claim Hr34d:
Rlt r34 d.
An
exact proof term for the current goal is
(andER ((r34 ∈ R ∧ Rlt 0 r34) ∧ Rlt r34 c) (Rlt r34 d) Hr34).
We prove the intermediate
claim Hr34left:
(r34 ∈ R ∧ Rlt 0 r34) ∧ Rlt r34 c.
An
exact proof term for the current goal is
(andEL ((r34 ∈ R ∧ Rlt 0 r34) ∧ Rlt r34 c) (Rlt r34 d) Hr34).
We prove the intermediate
claim Hr34c:
Rlt r34 c.
An
exact proof term for the current goal is
(andER (r34 ∈ R ∧ Rlt 0 r34) (Rlt r34 c) Hr34left).
We prove the intermediate
claim Hr34pair:
r34 ∈ R ∧ Rlt 0 r34.
An
exact proof term for the current goal is
(andEL (r34 ∈ R ∧ Rlt 0 r34) (Rlt r34 c) Hr34left).
We prove the intermediate
claim Hr34R:
r34 ∈ R.
An
exact proof term for the current goal is
(andEL (r34 ∈ R) (Rlt 0 r34) Hr34pair).
We prove the intermediate
claim Hr34pos:
Rlt 0 r34.
An
exact proof term for the current goal is
(andER (r34 ∈ R) (Rlt 0 r34) Hr34pair).
We prove the intermediate
claim Hex:
∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 r12 ∧ Rlt r3 r34.
Apply Hex to the current goal.
Let r3 be given.
Assume Hr3.
We prove the intermediate
claim Hr3lt34:
Rlt r3 r34.
An
exact proof term for the current goal is
(andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 r12) (Rlt r3 r34) Hr3).
We prove the intermediate
claim Hr3left:
(r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 r12.
An
exact proof term for the current goal is
(andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 r12) (Rlt r3 r34) Hr3).
We prove the intermediate
claim Hr3lt12:
Rlt r3 r12.
An
exact proof term for the current goal is
(andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 r12) Hr3left).
We prove the intermediate
claim Hr3pair:
r3 ∈ R ∧ Rlt 0 r3.
An
exact proof term for the current goal is
(andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 r12) Hr3left).
We prove the intermediate
claim Hr3R:
r3 ∈ R.
An
exact proof term for the current goal is
(andEL (r3 ∈ R) (Rlt 0 r3) Hr3pair).
We prove the intermediate
claim Hr3pos:
Rlt 0 r3.
An
exact proof term for the current goal is
(andER (r3 ∈ R) (Rlt 0 r3) Hr3pair).
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
An
exact proof term for the current goal is
(Rlt_tra r3 r12 a Hr3lt12 Hr12a).
An
exact proof term for the current goal is
(Rlt_tra r3 r12 b Hr3lt12 Hr12b).
An
exact proof term for the current goal is
(Rlt_tra r3 r34 c Hr3lt34 Hr34c).
An
exact proof term for the current goal is
(Rlt_tra r3 r34 d Hr3lt34 Hr34d).