tactic.interactive.linarith source