proposition: Theorem spec_succ: forall n, [succ n] = [n] + 1.
proof: Proof. intros x. rewrite succ_fold. destr_t x as (n,x). generalize (ZnZ.spec_succ_c x); destruct ZnZ.succ_c. intros. rewrite spec_mk_t. assumption. intros. unfold interp_carry in *. rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen