# Total order

## Definition

Let $$(S, \mathcal{R})$$ be a relational structure. Then $$\mathcal{R}$$ is a total order on $$S$$ if and only if:

$$\mathcal{R}$$ is an ordering:
$$\mathcal{R}$$ is reflexive:
$$\forall x \in S : x{\mathcal{R}}x$$
$$\mathcal{R}$$ is transitive:
$$\forall x,y,z \in S : x{\mathcal{R}}y \wedge y{\mathcal{R}}z \Rightarrow x{\mathrel{R}}z$$
$$\mathcal{R}$$ is anti-symmetric:
$$\forall x,y \in S : x{\mathcal{R}}y \wedge y{\mathcal{R}}x \Rightarrow x = y$$
$$\mathcal{R}$$ is connex:
$$\forall x,y \in S : x{\mathcal{R}}y \vee y{\mathcal{R}}x$$

## Axioms

order_refl: ?x ≤ ?x
order_trans: ?x ≤ ?y $$\Longrightarrow$$ ?y ≤ ?z
order_antisym: ?x ≤ ?y $$\Longrightarrow$$ ?y ≤ ?x $$\Longrightarrow$$ ?x = ?y
linear: ?x ≤ ?y $$\vee$$ ?y ≤ ?x
THEOREM    $$\forall x,y \in S : (x \le y \Rightarrow P) \wedge (y \le x \Rightarrow P) \Rightarrow P$$
le_cases:
(?x ≤ ?y $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?y ≤ ?x $$\Longrightarrow$$ ?P) $$\Longrightarrow$$ ?P

Proof available

THEOREM    \begin{alignat}{3} \forall x,y,z \in S :&\ (x \le y \wedge y \le z \Rightarrow P)&&\ \wedge\\ &\ (x \le z \wedge z \le y \Rightarrow P)&&\ \wedge\\ &\ (y \le x \wedge x \le z \Rightarrow P)&&\ \wedge\\ &\ (y \le z \wedge z \le x \Rightarrow P)&&\ \wedge\\ &\ (z \le x \wedge x \le y \Rightarrow P)&&\ \wedge\\ &\ (z \le y \wedge y \le x \Rightarrow P)&& \Rightarrow P \end{alignat}
le_cases3:
(?x ≤ ?y $$\Longrightarrow$$ ?y ≤ ?z $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?y ≤ ?x $$\Longrightarrow$$ ?x ≤ ?z $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?x ≤ ?z $$\Longrightarrow$$ ?z ≤ ?y $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?z ≤ ?y $$\Longrightarrow$$ ?y ≤ ?x $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?y ≤ ?z $$\Longrightarrow$$ ?z ≤ ?x $$\Longrightarrow$$ ?P) $$\Longrightarrow$$
(?z ≤ ?x $$\Longrightarrow$$ ?x ≤ ?y $$\Longrightarrow$$ ?P) $$\Longrightarrow$$ ?P

Proof available