proposition: Theorem evenb_double_conv : forall n, exists k, n = if evenb n then double k else S (double k).
proof: Proof. MProof. Admitted. Theorem even_bool_prop : forall n, evenb n = true <-> exists k, n = double k. MProof. intros n. T.split. - intros H. elim (evenb_double_conv n) &> [i: \k Hk]. rewrite Hk. rewrite H. mexists k. T.reflexivity. - pintros [| \k Hk]. rewrite Hk. apply evenb_double. Qed.