proposition: Lemma is_even_spec x : if is_even x then φ x mod 2 = 0 else φ x mod 2 = 1.
proof: Proof. rewrite is_even_bit. generalize (bit_0_spec x); case bit; simpl; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63