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

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

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