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