Stream: math-comp users

Topic: ✔ how to do remember ... as

view this post on Zulip walker (Nov 05 2022 at 10:23):

What is the mathcomp idiomatic way of doing remember (f x) as y ?
The reason is that I want to do induction over y.

What I don't like about remember (f x) as y is that it creates a proposition y = f x with automaticlly generated name that I cannot control.

view this post on Zulip Ana de Almeida Borges (Nov 05 2022 at 11:57):

move eqfxy: (f x) => y.

view this post on Zulip Notification Bot (Nov 05 2022 at 13:09):

walker has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC