CoInduction in Coq
<|reference_start|>CoInduction in Coq: We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.<|reference_end|>
@article{bertot2006coinduction,
    title={CoInduction in Coq},
    author={Yves Bertot (INRIA Sophia Antipolis)},
    journal={arXiv preprint arXiv:cs/0603119},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0603119},
    primaryClass={cs.LO}
}