a small lemma about the constant RV

[affeldt-aist]

Note that there is only one lemma: the other one is actually an instance of pfwd1_const_RV from your PR #219 @t6s

[t6s]

What about stating an equivalence instead of inference?

Lemma dirac_const_RV {R : realType} (U T : finType) (P : R.-fdist U)
  (X : {RV P -> T}) (a : T) :
  `Pr[X = a] = 1 <-> ({in [set u | P u != 0], X =1 const_RV P a}).
Proof.
rewrite pfwd1E Pr_to_cplt (rwP eqP) -eqr_opp opprB subr_eq addrC subrr.
split.
  move=> /eqP + u; rewrite inE => + Pu0.
  have [->//|Xua] := eqVneq (X u) a.
  move/eqP; rewrite psumr_eq0// => /allP /(_ u).
  by rewrite mem_index_enum !inE Xua/= (negPf Pu0) => /(_ erefl).
move=> H; apply/eqP/Pr_set0P => u; have := H u; rewrite !inE/=.
have [//|?] := eqVneq (P u) 0.
by move/(_ erefl) ->; rewrite /const_RV/cst/= eqxx.
Qed.

[t6s]

The proof can be shortened:

Proof.
move=> /eqP + u; rewrite inE => + Pu0. 
have [->//|Xua] := eqVneq (X u) a.
suff: `Pr[ (X) = (a) ] != 1 by move/negPf ->.
rewrite pfwd1E Pr_to_cplt -eqr_opp opprB subr_eq addrC subrr psumr_neq0//.
by apply/hasP; exists u => //; rewrite !inE Xua/= fdist_gt0.
Qed.