Add Linear Iff definition.
Add some ltacs and examples.