proposition: Lemma spec_double_modn1_aux : forall n a b, double_modn1 n a b = snd (double_divn1 n a b).
proof: Proof. intros n a b;unfold double_divn1,double_modn1. rewrite spec_compare; case Z.compare_spec; rewrite spec_0; intros H2; auto with zarith. apply spec_double_modn1_0. apply spec_double_modn1_0. rewrite spec_double_modn1_p. destruct (double_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n (w_add_mul_div (w_head0 b) w_0 (high n a)) a (double_0 w_0 n));simpl;trivial. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase