proposition: Lemma spec_double_modn1 : forall n a b, 0 < [|b|] -> [|double_modn1 n a b|] = [!n|a!] mod [|b|].
proof: Proof. intros n a b H;assert (H1 := spec_double_divn1 n a H). assert (H2 := spec_double_modn1_aux n a b). rewrite H2;destruct (double_divn1 n a b) as (q,r). simpl;apply Zmod_unique with (double_to_Z w_digits w_to_Z n q). auto with zarith. destruct H1 as (h1,h2);rewrite h1;ring. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase