Add basic lemmas to exploit hypotheses in behavior

This ensures all hypotheses in behavior have corresponding trivial lemmas in analysis/facts/all that enable to exploit them. This also makes the code more robust to potential changes in the precise way these hypotheses are stated.

added 1 commit

• b7b7fd0f - Add basic lemmas to exploit hypotheses in behavior

Compare with previous version

Thanks, Pierre!

Quick question — I don't think I quite understand the comments:

Make hypothesis more easier to discover.

Who should discover these? Easier to discover for proof automation, or by the human user? Could you perhaps clarify this?

resolved all threads

added 1 commit

• 37b23690 - to squash: tweak comments and section flow

Compare with previous version

Thanks for fixing the comments, feel free to squash.

added 3 commits

• af4fb1db - 1 commit from branch master
• 092ba9ac - Add basic lemmas to exploit hypotheses in behavior
• 05a6b64e - to squash: tweak comments and section flow

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for 05a6b64e succeeds

aborted the automatic merge because source branch was updated

added 1 commit

• 0b6a5f8a - resolve spelling issues

Compare with previous version

enabled an automatic merge when the pipeline for 0b6a5f8a succeeds

merged