proposition: Lemma _power_mod_spec: forall w t p, [|w|] = t mod [|b|] -> [|_power_mod w p|] = (Zpower_pos [|w|] p) mod [|b|].
proof: Proof. intros w2 t p; elim p; simpl; auto with zarith. intros p' Rec H. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t [|b|]); auto with zarith. replace (xI p') with (p' + p' + 1)%positive. repeat rewrite Zpower_pos_is_exp; auto with zarith. pose (t1 := [|_power_mod w2 p'|]). rewrite _mul_mod_spec with (t1 := t1 * t1) (t2 := t); auto with zarith. rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. rewrite Rec; auto with zarith. assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). intros p1; unfold Zpower_pos; simpl; ring. rewrite <- Zmult_mod; auto with zarith. rewrite Zmult_mod; auto with zarith. rewrite Zmod_mod; auto with zarith. rewrite <- Zmult_mod; auto with zarith. simpl; unfold t1; apply _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. rewrite xI_succ_xO; rewrite <- Pplus_diag. rewrite Pplus_one_succ_r; auto. intros p' Rec H. replace (xO p') with (p' + p')%positive. repeat rewrite Zpower_pos_is_exp; auto with zarith. rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. rewrite Rec; auto with zarith. rewrite <- Zmult_mod; auto with zarith. rewrite <- Pplus_diag; auto. intros H. assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). intros p1; unfold Zpower_pos; simpl; ring. rewrite Zmod_small; auto with zarith. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t [|b|]); auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux