proposition: Lemma sub_exists (T : finType) (P1 P2 : pred T) : subpred P1 P2 -> [exists x, P1 x] -> [exists x, P2 x].
proof: Proof. move => H. case/existsP => x /H ?. apply/existsP. by exists x. Qed.
imports: mathcomp(all_ssreflect)