feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved

Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`