English
If U is right-unique for r, then from a to b and a to c via ReflTransGen r, one can determine the order of b and c: either b reaches c or c reaches b.
Русский
Если U — правая уникальность для r, то из a до b и из a до c через ReflTransGen r следует, что либо b достигает c, либо c достигает b.
LaTeX
$$$ \forall {α} {r : α \to α \to Prop} {a b c : α} (U : Relator.RightUnique r), \mathrm{ReflTransGen} r a b \to \mathrm{ReflTransGen} r a c \to (\mathrm{ReflTransGen} r b c \lor \mathrm{ReflTransGen} r c b)$$$
Lean4
theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a b) (ac : ReflTransGen r a c) :
ReflTransGen r b c ∨ ReflTransGen r c b := by
induction ab with
| refl => exact Or.inl ac
| tail _ bd IH =>
rcases IH with (IH | IH)
· rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
· exact Or.inr (single bd)
· cases U bd be
exact Or.inl ec
· exact Or.inr (IH.tail bd)
