proposition: Lemma exists_witness_ok : forall e f s, Proper (SP.Equal ==> eq) f -> exists_witness f s = Some e -> SSP.In e s.
proof: Proof. intros e f s HP H. unfold exists_witness in H. apply SSPWEqP.MP.Dec.F.mem_2. apply SSPWEqP.choose_mem_1 in H. rewrite SSPWEqP.filter_mem in H; try assumption. apply andb_true_iff in H. induction H. assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets