proposition: Lemma spec_ww_is_even : forall x, if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.
proof: Proof. clear spec_more_than_1_digit. intros x; case x; simpl ww_is_even. reflexivity. simpl. intros w1 w2; simpl. unfold base. rewrite Zplus_mod by zarith. rewrite (fun x y => (Zdivide_mod (x * y))). rewrite Z.add_0_l; rewrite Zmod_mod by zarith. apply spec_w_is_even; zarith. apply Z.divide_mul_r; apply Zpower_divide; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase