| Hello Frédéric, thanks for the suggestion – we always value hints about which lemmas are missing in the standard library. In fact, the next release will see many additions to the SequenceProperties module. However, I am a little reluctant to add the lemma that you propose, since it is just proved by OBVIOUS. If you have an instance of this lemma in the context of a larger proof where the prover was unable to prove such a step, I'd be interested in hearing about it. Regards, Stephan
|