rsuffices tactic #
The rsuffices tactic is an alternative version of suffices, that allows the usage
of any syntax that would be valid in an obtain block. This tactic just calls obtain
on the expression, and then rotate_left.
The rsuffices tactic is an alternative version of suffices, that allows the usage
of any syntax that would be valid in an obtain block. This tactic just calls obtain
on the expression, and then rotate_left.
Equations
- One or more equations did not get rendered due to their size.