m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) (↑finAddFlip { val := n, isLt := (_ : n < n + 1) }) = 0
m n : ℕ
⊢ ↑(finRotate (n + 1)) { val := n, isLt := (_ : n < n + 1) } = { val := 0, isLt := (_ : 0 < Nat.succ n) }
dsimp [finRotate_succ]
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) { val := n - n, isLt := (_ : n - n < 1 + n) } = 0
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) (↑finAddFlip { val := n, isLt := (_ : n < n + 1) }) = 0
rw [finAddFlip_apply_mk_right le_rfl]
no goals
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) { val := n - n, isLt := (_ : n - n < 1 + n) } = 0
simp