Surreal numbers in Coq

Surreal Numbers form a totally ordered (commutative) Field, containing copies of the reals and (all) the ordinals. I have encoded most of the Ring structure of surreal numbers in Coq. This encoding relies on Aczel's encoding of set theory in type theory. This paper discusses in particular the definitional or proving points where I had to diverge from Conway's or the most natural way, like separation of simultaneous induction-recursion into two inductions, transforming the definition of the order into a mutually inductive definition of "at most" and "at least" and fitting the rather complicated induction/recursion schemes into the type theory of Coq.