proposition: Theorem silly_ex : (forall n, evenb n = true -> oddb (S n) = true) -> evenb 3 = true -> oddb 4 = true.
proof: Proof. MProof. Admitted. Theorem silly3_firsttry : forall (n : nat), true = beq_nat n 5 -> beq_nat (S (S n)) 7 = true. MProof. intros n H. simpl. symmetry. simpl. apply H. Qed.