proposition: Lemma equiv_conv p (a b : T) : a <| p |> b = a <& p &> b.
proof: Proof. apply: S1_inj. rewrite [LHS](@affine_conv NaryConv_sort__canonical__isConvexSpace__ConvexSpace)/=. by rewrite [RHS](@affine_conv NaryConv_sort__canonical__isConvexSpace__ConvexSpace). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex