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