fact: Definition compare : t -> t -> comparison := Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in compare_folded.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen