Question

When proving an iff (<==>), is there a nice way to prove this by proving each side of the implication separately without making 2 different lemmas?

Answer

Here are two ways to prove A <==> B:

if A {
  // prove B...
}
if B {
  // prove A...
}

Another way is

calc {
  A;
==
  // ...
==
  B;
}