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

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

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

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

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

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