Theorem: v_b6_of_v_a3_a (test/testelin.lean)

State before:
q : ℕ
h : ↑q ≥ 2
⊢ ↑q ≥ 1
Tactic:
elinarith
State after:
no goals