fact: Definition comparenm n m wx wy := let mn := Nat.max n m in let d := diff n m in let op := make_op mn in ZnZ.compare (castm (diff_r n m) (extend_tr wx (snd d))) (castm (diff_l n m) (extend_tr wy (fst d))).
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen