proposition: Lemma even_double_conv : forall n, exists k, n = if even n then double k else S (double k).
proof: Proof. Admitted. Theorem even_bool_prop : forall n, even n = true <-> Even n. Proof. intros n. split. - intros H. destruct (even_double_conv n) as [k Hk]. rewrite Hk. rewrite H. exists k. reflexivity. - intros [k Hk]. rewrite Hk. apply even_double. Qed.