On 04/11/2019 02:01, David Topham wrote:
Those two don't seem to get along! Probably my error and sorry to be burdening you with debugging due to partial understanding on my part.
you need ⌜sum (pow r)⌝ and now you are in the reals, / instead of Div, so: ⌜λ n⦁ ∀ r⦁ sum (pow r) n = 1.0 - pow r (n + 1) / (1.0 - r)⌝; Roger
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
