Is there a way to provide a witness to a goal of the form [exists _, _]
without first applying existsP
? Basically something analogous to rewriting with a hypothesis H : b = true
when our goal is b && b'
instead of going through apply/andP; split=> //
.
Not that I know of, but we could add
Lemma existsb (T : finType) (P : {pred T}) (x : T) : P x -> [exists x, P x].
Proof. by move=> Px; apply/existsP; exists x. Qed.
Arguments existsb {T P}.
So that rewrite (existsb x).
would do what you want?
Yes! Thanks
Cyril Cohen has marked this topic as resolved.
@Ana de Almeida Borges added: https://github.com/math-comp/math-comp/pull/941
Awesome!
Last updated: Oct 13 2024 at 01:02 UTC