Stream: Coq users

Topic: greater than relation


view this post on Zulip pianke (Oct 03 2023 at 06:10):

H: S sum = 1 *  a
H1:  (1 <?  a) = true

May i derive (1 = sum) from above.( While a sum :nat)

view this post on Zulip Quentin VERMANDE (Oct 03 2023 at 06:47):

Maybe I misunderstand the notation (_ <? _), but here, if you want sum to be 1, then ~a has to be 2 because of hypothesis H, which is not a consequence of your hypotheses (unless (x <? y) means e.g. y = S x), so I would say no (for instance, sum=2 and ~a=3 would satisfy your hypotheses).


Last updated: Jun 23 2024 at 04:03 UTC