proposition: Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y).
proof: Proof. unfold div_eucl, to_Z. intros [x | x] [y | y]. generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). { break_nonneg x px EQx; break_nonneg y py EQy; rewrite NN.spec_eqb, NN.spec_0; cbn. - intros [= EQq EQr]. rewrite EQr, EQq. cbn. now rewrite NN.spec_0. - intros [= EQq EQr]. rewrite EQr, EQq. cbn. now rewrite NN.spec_0. - intros [= EQq EQr]. rewrite EQr, ?NN.spec_eqb, ?EQy, ?NN.spec_0, <- ?EQx. cbn. now rewrite ?EQq, NN.spec_0. - pose proof (B := Z.pos_div_eucl_bound px (Zpos py)). destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). cbn in B. intros [= EQq EQr]. break_nonneg r pr' EQr'. + subst. cbn. now rewrite NN.spec_0. + subst. rewrite NN.spec_eqb, EQy, NN.spec_0. cbn. rewrite NN.spec_succ, NN.spec_sub, EQy, EQr', <- Z.pos_sub_opp. cbn. f_equal. rewrite Z.pos_sub_gt; lia. } generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). { break_nonneg x px EQx; break_nonneg y py EQy; rewrite NN.spec_eqb, NN.spec_0; cbn. - intros [= EQq EQr]. rewrite EQr, EQq. cbn. now rewrite NN.spec_0. - intros [= EQq EQr]. rewrite EQr, EQq. cbn. now rewrite NN.spec_0. - intros [= EQq EQr]. rewrite EQr, ?NN.spec_eqb, ?EQy, ?NN.spec_0. cbn. now rewrite NN.spec_0, <- ?Pos2Z.opp_pos, ?EQx, ?EQq. - pose proof (B := Z.pos_div_eucl_bound px (Zpos py)). destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). cbn in B. intros [= EQq EQr]. break_nonneg r pr' EQr'. + subst. cbn. now rewrite NN.spec_0. + subst. rewrite NN.spec_eqb, EQy, NN.spec_0. cbn. rewrite NN.spec_succ, NN.spec_sub, EQy, EQr'. cbn. f_equal. rewrite Z.pos_sub_gt; lia. } generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; try (injection 1 as -> ->; auto). simpl. intros <-; auto. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig