Add lemma `StronglySorted_app_iff`

This merge request adds the lemma StronglySorted_app_iff (and the corollary StronglySorted_app), and rewrites the existing *_app lemmas as a corollary of StronglySorted_app_iff.

added 1 commit

• 73e36d32 - Implement *_iff lemma and rewrite other as corollary

Compare with previous version

changed title from Add lemma StronglySorted_app to Add lemma StronglySorted_app{+_iff+}

changed the description

added 4 commits

• 73e36d32...e3a6f3ef - 2 commits from branch iris:master
• 802ed00d - Add lemma `StronglySorted_app`
• 38b86934 - Implement *_iff lemma and rewrite other as corollary

Compare with previous version

added 5 commits

• 38b86934...96ef0cd6 - 4 commits from branch iris:master
• 7ee39617 - Merge branch 'master' into marijnvanwezel/StronglySorted_app

Compare with previous version

added 1 commit

• 2c33ca58 - Remove remnant of merge conflict

Compare with previous version

I proposed some renames, that should make things consistent with the consensus in !394 (merged) That is, do not use _iff, but use _{1,2} for the non ↔ versions.

@jung Can you check my proposal is indeed consistent?

We discussed this in our meeting, @robbertkrebbers will take care of these edits (so please don't push to your branch for now :)

added 15 commits

• 2c33ca58...0dbb3948 - 12 commits from branch iris:master
• 615f3f66 - Add lemma `StronglySorted_app`
• 24c0085e - Renames and make use of `set_solver` to shorten proof.
• e2ef2933 - Tweak CHANGELOG.

Compare with previous version

resolved all threads

@jung As discussed, I renamed the _1_X lemmas into something where X is informative instead of a number 1..3.

I also added a similar lemma for StronglySorted_cons. I am not sure it's too useful to add the _1 and _2 versions here, since they are just the constructors/inversion.

Please review.

added 1 commit

• f7f5a013 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• c12e2b75 - Do not export `sets` for `sorting`

Compare with previous version