proposition: Theorem spec_modulo: forall x y, [modulo x y] = [x] mod [y].
proof: Proof. intros x y. unfold modulo. rewrite spec_eqb, spec_compare, spec_0. case Z.eqb_spec. intros ->; rewrite ?spec_0. destruct [x]; auto. intro H'. assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. case Z.compare_spec; rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith. rewrite H0; symmetry; apply Z_mod_same; auto with zarith. symmetry; apply Zmod_small; auto with zarith. generalize (spec_pos x); auto with zarith. apply spec_mod_gt; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen