proposition: Theorem sillyfun1_odd_FAILED : forall (n : nat), sillyfun1 n = true -> odd n = true.
proof: Proof. intros n eq. unfold sillyfun1 in eq. destruct (n =? 3). Abort. Theorem sillyfun1_odd : forall (n : nat), sillyfun1 n = true -> odd n = true. Proof. intros n eq. unfold sillyfun1 in eq. destruct (n =? 3) eqn:Heqe3. - apply eqb_true in Heqe3. rewrite -> Heqe3. reflexivity. - destruct (n =? 5) eqn:Heqe5. + apply eqb_true in Heqe5. rewrite -> Heqe5. reflexivity. + discriminate eq. Qed.