proposition: Lemma affine_S1 : affine (@S1 A).
proof: Proof. move=> p x y. have /RleP[p0|p0] := prob_ge0 p; last first. by rewrite (_ : p = 0%:pr) ?conv0 //; exact/val_inj. have /RleP[p1|p1] := prob_le1 p; last first. by rewrite (_ : p = 1%:pr) ?conv1 //; exact/val_inj. rewrite convptE (scalept_gt0 _ _ p0) (@scalept_gt0 (Prob.p p).~). exact/RltP/onem_gt0/RltP. move=> mp0; congr (_ *: _) => /=. apply/val_inj => /=; rewrite !mulR1. by rewrite RplusE onemKC. by congr (_ <| _ |> _); apply val_inj; rewrite /= !mulR1 addRC subRK divR1. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist