proposition: Theorem evenb_double_conv : forall n, exists k, n = if evenb n then double k else S (double k).
proof: Proof. Admitted. Theorem even_bool_prop : forall n, evenb n = true <-> exists k, n = double k. Proof. intros n. split. - intros H. destruct (evenb_double_conv n) as [k Hk]. rewrite Hk. rewrite H. exists k. reflexivity. - intros [k Hk]. rewrite Hk. apply evenb_double. Qed.
imports: Tactics