proposition: Lemma is_even_bit i : is_even i = negb (bit i 0).
proof: Proof. unfold is_even. replace (i land 1) with (b2i (bit i 0)). - case bit; auto. - apply bit_ext; intros n. rewrite bit_b2i, land_spec, bit_1. generalize (eqb_spec n 0). case (n =? 0)%uint63; auto. + intros(H,_); rewrite andb_true_r, H; auto. + rewrite andb_false_r; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63