⊢ ∃ j, ∀ (i : LeftMoves (moveRight star j)), moveLeft (moveRight star j) i ⧏ 0
⊢ star ⧏ 0
rw [lf_zero]
⊢ ∀ (i : LeftMoves (moveRight star default)), moveLeft (moveRight star default) i ⧏ 0
⊢ ∃ j, ∀ (i : LeftMoves (moveRight star j)), moveLeft (moveRight star j) i ⧏ 0
use default
no goals
⊢ ∀ (i : LeftMoves (moveRight star default)), moveLeft (moveRight star default) i ⧏ 0
rintro ⟨⟩
⊢ ∃ i, ∀ (j : RightMoves (moveLeft star i)), 0 ⧏ moveRight (moveLeft star i) j
⊢ 0 ⧏ star
rw [zero_lf]
⊢ ∀ (j : RightMoves (moveLeft star default)), 0 ⧏ moveRight (moveLeft star default) j
⊢ ∃ i, ∀ (j : RightMoves (moveLeft star i)), 0 ⧏ moveRight (moveLeft star i) j
use default
no goals
⊢ ∀ (j : RightMoves (moveLeft star default)), 0 ⧏ moveRight (moveLeft star default) j
rintro ⟨⟩