fact: Definition pheight p := Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))).
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen