Stream: Coq users

Topic: le_antisymm


view this post on Zulip lilia Nejoua (Oct 31 2023 at 15:48):

hello I have a homework assignment can you help me prove a theorem I a stuck in one place

view this post on Zulip lilia Nejoua (Oct 31 2023 at 15:49):

i don’t now if I should ask for help in this forum

view this post on Zulip Gaëtan Gilbert (Oct 31 2023 at 15:51):

https://dontasktoask.com/

view this post on Zulip lilia Nejoua (Oct 31 2023 at 15:56):

I want to demonstrate the theorem le_antisymm (they advised us to do a proof by case on m and then reason in such a way as to be able to use succ_le_mono for the moment what I did was induction on n then j 'have destruct n then reflexivity I have re destruct m I must now prove 0=1 with the hypothesis n: 0<=0 and J: 1<=0

view this post on Zulip lilia Nejoua (Oct 31 2023 at 16:14):

1173062A-D70B-4226-B9BA-EB212AFCA727.png

view this post on Zulip Julio Di Egidio (Oct 31 2023 at 16:25):

Hint: you can do destruct or inversion on a false hypothesis.

view this post on Zulip Pierre Rousselin (Oct 31 2023 at 16:35):

There should be a lemma somewhere saying that no successor of an integer is less than or equal to 0. This means that from 1 <= 0 one can prove false, hence anything.


Last updated: Jun 13 2024 at 19:02 UTC