proposition: Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
proof: Proof. intros x y. unfold div_eucl. rewrite spec_eqb, spec_compare, spec_0. case Z.eqb_spec. intros ->. rewrite spec_0. cbn. rewrite ?ZnZ.spec_0. destruct [x]; auto. intros H'. assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. case Z.compare_spec; intros Cmp; rewrite ?spec_0, ?spec_1; intros; auto with zarith. rewrite Cmp; generalize (Z_div_same [y] (Z.lt_gt _ _ H)) (Z_mod_same [y] (Z.lt_gt _ _ H)); unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto). generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt); unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. generalize (spec_div_gt _ _ (Z.lt_gt _ _ Cmp) H); auto. unfold Z.div, Z.modulo; case Z.div_eucl; case div_gt. intros a b c d (H1, H2); subst; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen