proposition: Lemma spec_w_2: [|w_2|] = 2.
proof: Proof. unfold w_2; rewrite spec_w_add; rewrite spec_w_1; simpl. apply Zmod_small; split; auto with zarith. rewrite <- (Z.pow_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase