proposition: Theorem spec_max : forall n m, [max n m] = Z.max [n] [m].
proof: Proof. intros. unfold max, Z.max. rewrite spec_compare; destruct Z.compare; reflexivity. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen