Stream: Coq users

Topic: equal values


view this post on Zulip pianke (Mar 28 2023 at 17:08):

I have list of two or more natural numbers.l=(k1::k2::t).These ks may be same or different because i have no hypothesis related to this.Only available information is H2:z1=k1 H3:z2=k2. z1=z2 is possible? (only when k1=k2 ,i have no information about this. To avid this i have to add no duplication )

view this post on Zulip Laurent Théry (Mar 28 2023 at 17:54):

you shoudl do Absurd (k1 = k2). One subgoal is solved by the fact that there is no duplication, the second one because of available information.


Last updated: Mar 29 2024 at 13:01 UTC