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: Oct 13 2024 at 01:02 UTC