proposition: Lemma spec_double_modn1_p : forall n r h l , double_modn1_p n r h l = snd (double_divn1_p n r h l).
proof: Proof. induction n;simpl;intros;trivial. unfold double_modn1_p_aux, double_divn1_p_aux. destruct(double_split w_0 n h)as(hh,hl);destruct(double_split w_0 n l) as (lh,ll). rewrite (IHn r hh hl);destruct (double_divn1_p n r hh hl) as (qh,rh). rewrite IHn;simpl;destruct (double_divn1_p n rh hl lh);trivial. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase