I feel like I'm missing a simple tactic. How can I convert a goal of the form `S x = S y`

into `x = y`

for arbitrary expressions `x, y`

and constructor `S`

? What about `f x = f y`

where `f`

is not necessarily an invertible function? I know I can achieve it with `rewrite`

if I need to, using `enough`

or `assert`

to get to that point, but I feel like there's a better way.

`apply f_equal`

(or just the `f_equal`

tactic, for higher arity).

can you help me how i can prouve that with succ_le_mono

1987A872-1DF8-41A7-B988-8C86DBE86F08.png

@lilia Nejoua What is *that*? Also, to make it easier for us to help you, you should 1) post any new question in a *new* topic (go to the left, click ⋮ and "new topic"; 2) instead of screenshots, provide written code (enclosed in single backticks ` or triple backticks ```), so that people can copy-paste your code and experiment with it.

Also don't post the same question twice in two different topics.

This looks like an assignent from some class..

@Théo Zimmermann @Cyril Cohen

Yes, that's an assignment for my class (first year undergraduate). It's ok that the students ask questions here, I guess ("Beginner questions welcome"), and I gave them the link. It's true that this question was clumsily asked, but this is also something to learn.

maybe good to ask your students to flag up that it's a homework question (so people know they ideally shouldn't solve everything completely, but rather give learning-friendly hints)

indeed we would like to be welcoming to these kind of questions, but also help those that ask them with meta-problems like structuring the question.

Last updated: Jun 22 2024 at 15:01 UTC