proposition: Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.
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. assumption. exfalso. unfold interp_carry in *. generalize (ZnZ.spec_to_Z x) (ZnZ.spec_to_Z y); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen