fact: Fixpoint plusn0 n : n + 0 = n := match n return (n + 0 = n) with | 0 => eq_refl 0 | S n1 => let v := S n1 in eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1) end.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic