Add validI lemmas for discrete RAs
Our discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the Prop-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
!558 (merged) added the lemma for frac, but other RAs are still missing:
-
gset_disj -
coPset,coPset_disj -
sts -
dfrac