Make bv_automata fallible (#670)

Currently, `bv_automata` does not fail if the goal is false, because
`native_decide` doesn't fail, it produces an ill-typed proof.

On consequence is that it is awkward to use `bv_automata` in a tactic
such as `bv_auto`, since it relied on tactics to fail to be able to try
the next tactic (cf issue #660) It also give an error that is not
helpful at all after the proof is complete.

This PR is a proof of concept that modifies the implementation of
`native_decide` to check that the problem is solved by the decision
procedure before constructing the proof object.