proposition: Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]).
proof: Proof. intros. destruct (Z.le_gt_cases [y] [x]). rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto. rewrite Z.max_l; auto with zarith. apply spec_sub0; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen