proposition: Lemma spec_double_modn1_0 : forall n r x, double_modn1_0 n r x = snd (double_divn1_0 n r x).
proof: Proof. induction n;simpl;intros;trivial. unfold double_modn1_0_aux, double_divn1_0_aux. destruct (double_split w_0 n x) as (hh,hl). rewrite (IHn r hh). destruct (double_divn1_0 n r hh) as (qh,rh);simpl. rewrite IHn. destruct (double_divn1_0 n rh hl);trivial. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase