proposition: Theorem spec_div: forall x y, [div x y] = [x] / [y].
proof: Proof. intros x y; unfold div; generalize (spec_div_eucl x y); case div_eucl; simpl fst. intros xx yy; unfold Z.div; case Z.div_eucl; intros qq rr H; injection H; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen