proposition: Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0.
proof: Proof. intros x. rewrite pred_fold. destr_t x as (n,x). intros H. generalize (ZnZ.spec_pred_c x); destruct ZnZ.pred_c as [y|y]; intros H'. rewrite spec_reduce. unfold interp_carry in H'. generalize (ZnZ.spec_to_Z y); auto with zarith. exact spec_0. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen