Paper-Proof/paperproof

Calc command doesn't work

Closed this issue · 1 comments

antonkov commented 
example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
  have h3 := calc
      m + 3 ≤ 2 * n - 1 := by gcongr
      _ ≤ 2 * 5 - 1 := by gcongr
      _ = 9 := by norm_num
  clear h1 h2
  linarith

doesn't work

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/paperproof.20discussion/near/397816033