define fsdist_conv using the convType of R

[t6s]

The convex space structure on fsdist has been provided first by defining fsdist_convn and then fsdist_conv using it, introducing many complications in the proofs of basic lemmas.

This PR corrects it, defining the binary fsdist_conv using the convex structure on R, and using the generic Convn instead of defining fsdist_convn.

NB:

• fsdist_convA is removed; this is used in proba_monad_model.v in monae
• fsdist_convE is changed; this probably affects its use in altprob_model.v in monae

[affeldt-aist]

We maybe need to make sure that monae is not broken before merging.

[t6s]

The removal of fsdist_convA surely breaks the current monae (but avoidable by https://github.com/affeldt-aist/monae/pull/122 ).

fsdist_convE also breaks a proof in altprob_model:

Example gcmAP_choice_nontrivial (p q : prob) :
  p <> q ->
  (* Ret = hierarchy.ret *)
  Ret true <|p|> Ret false <>
  Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
Proof.
apply contra_not.
rewrite !gcm_retE /Choice /= => /(congr1 (@NECSet.car _)).
rewrite !necset_convType.convE !conv_cset1 /=.
move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
by rewrite !fsdist_convE !fsdist1xx !mulR1 fsdist10 ?mulR0 ?addR0//;
  [exact: val_inj|exact/eqP].
Qed.

Inserting avgRE in the last rewrite solves the issue:

by rewrite !fsdist_convE ?avgRE !fsdist1xx !mulR1 fsdist10 ?mulR0 ?addR0//;

I am also okay to revert the change in (the type of) fsdist_convE to keep the compatibility.