Stream: Coq users

Topic: relation between numbers


view this post on Zulip zohaze (Mar 23 2023 at 10:57):

I have following natural numbers and their list. From this minimun information ,may i derive k=m?
mylist : b::b'::l<>[]
H: k=b
H1: m=b'
k=m or b=b' or i should have any information about the relation between b & b'?

view this post on Zulip Alex Loiko (Mar 23 2023 at 11:12):

The last hypothesis is that k=m \/ b=b', right? If it's named H2: k=m \/ b=b' you can do elim H2: congruence. to prove k=m. Otherwise you don't have enough information.

view this post on Zulip Paolo Giarrusso (Mar 23 2023 at 11:23):

; not : right?

view this post on Zulip Alex Loiko (Mar 23 2023 at 14:30):

Paolo Giarrusso said:

; not : right?

Yes, typo, edited.


Last updated: Mar 29 2024 at 04:02 UTC