proposition: Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1).
proof: Proof. rewrite Z.max_comm. destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)]. - apply spec_pred0; generalize (spec_pos x); auto with zarith. - apply spec_pred_pos; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen