proposition: Lemma _square_mod_spec: forall w t, [|w|] = t mod [|b|] -> [|_square_mod w|] = ([|w|] * [|w|]) mod [|b|].
proof: Proof. intros w2 t2 H; unfold _square_mod, wwb. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t2 [|b|]); auto with zarith. match goal with |- context[ww_compare ?x ?y] => change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y) end. rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare); case Z.compare_spec; intros H2; match goal with H: context[w_square_c] |- _ => generalize H; clear H end; autorewrite with w_rewrite. rewrite _w0_is_0. unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c. intros H2;rewrite H2; simpl. rewrite _w0_is_0; simpl. rewrite Z_mod_same; auto with zarith. generalize (high_zero (w_square_c w2)). unfold w_square_c; generalize (ZnZ.spec_square_c w2); case (ZnZ.square_c w2); simpl; auto with zarith. intros H3 _ _; rewrite <- H3; autorewrite with w_rewrite; auto. intros w4 w5. change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0; simpl. change (w_to_Z w4) with [|w4|]. change (w_to_Z w5) with [|w5|]. intros H2 H3 H4. assert (E1: [|w4|] = 0). apply H3. apply Z.lt_trans with (1 := H4). case (ZnZ.spec_to_Z b); auto with zarith. generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l; clear H4 H2; intros H4 H2. rewrite <- H2; rewrite Zmod_small. auto with zarith. case (ZnZ.spec_to_Z w5); auto with zarith. intros H2. match goal with |- context[split ?x] => generalize (split_correct x); case (split x); auto with zarith end. assert (F1: [[w_square_c w2]] < [|b|] * [|b|]). unfold w_square_c, ww_to_Z, w_digits, w_to_Z. rewrite ZnZ.spec_square_c. apply Zmult_lt_compat. case (ZnZ.spec_to_Z w2); auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. intros w4 w5; rewrite ww_lsl_n_spec by auto with zarith. intros H3. unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] => generalize (ZnZ.spec_div21 y z t); case (ZnZ.div21 y z t) end. rewrite b2n_spec; case (n_spec); auto. intros H4 H5 w6 w7 H6. case H6. auto with zarith. case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7. match type of H3 with ?X = ?Y => absurd (Y < X) end. apply Zle_not_lt; rewrite H3; auto with zarith. simpl ww_to_Z. match goal with |- ?X < ?Y + _ => apply Z.lt_le_trans with Y; auto with zarith end. apply Z.lt_trans with (2 ^ [|n|] * ([|b|] * [|b|])). apply Zmult_lt_compat_l; auto with zarith. rewrite Zmult_assoc. apply Zmult_lt_compat2. auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. unfold w_to_Z,w_digits;case (ZnZ.spec_to_Z w5). auto with zarith. clear H6; intros H7 H8. rewrite w_lsr_n_spec by auto with zarith. rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|])) by auto with zarith; rewrite Zmult_comm. rewrite <- ZnZ.spec_square_c. unfold w_square_c, ww_to_Z in H3; unfold w_digits,w_to_Z in H3. rewrite <- H3; simpl. rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x)); rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l by auto with zarith. rewrite Zplus_mod. rewrite Z_mod_mult. rewrite Zplus_0_l. rewrite Zmod_mod. rewrite Zmod_small. auto with zarith. split. auto with zarith. apply Zdiv_lt_upper_bound. auto with zarith. rewrite Zmult_comm; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux