proposition: Lemma spec_div_gt_aux : forall x y, [x] > [y] -> 0 < [y] -> let (q,r) := div_gt x y in [x] = [q] * [y] + [r] /\ 0 <= [r] < [y].
proof: Proof. intros x y. rewrite div_gt_fold. apply spec_iter; clear x y. intros n x y H1 H2. simpl. generalize (ZnZ.spec_div_gt x y H1 H2); destruct ZnZ.div_gt as [u v]. rewrite 2 spec_reduce. auto. intros n m x y H1 H2. cbv zeta beta. generalize (ZnZ.spec_div_gt x (DoubleBase.get_low (zeron n) (S m) y)). destruct ZnZ.div_gt as [u v]. intros H3; repeat rewrite spec_reduce. generalize (spec_get_endn n (S m) y x). rewrite !spec_mk_t. intros H4. rewrite H4 in H3; auto with zarith. intros n m x y H1 H2. generalize (spec_divn1 n (S m) x y H2). unfold wn_divn1; case DoubleDivn1.double_divn1. intros u v H3. rewrite spec_mk_t_w', spec_mk_t. rewrite <- !nmake_double in H3; auto. intros n m x y H1 H2; unfold div_gtnm. generalize (ZnZ.spec_div_gt (castm (diff_r n m) (extend_tr x (snd (diff n m)))) (castm (diff_l n m) (extend_tr y (fst (diff n m))))). case ZnZ.div_gt. intros xx yy HH. repeat rewrite spec_reduce_n. rewrite (spec_cast_l n m x), (spec_cast_r n m y). unfold to_Z; apply HH. rewrite (spec_cast_l n m x) in H1; auto. rewrite (spec_cast_r n m y) in H1; auto. rewrite (spec_cast_r n m y) in H2; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen