proposition: Lemma addptE a b (a0 : a != @Zero A) (b0 : b != Zero) : let p := [weight of a0] in let q := [weight of b0] in let x := [point of a0] in let y := [point of b0] in addpt a b = (p + q)%:pos *: (x <| ((p / (p + q))%:pos)%:pr |> y).
proof: Proof. move: a b => [p x|//] [pb y|//] /= in a0 b0 *. by congr (_ *: (_ <| _ |> _)); exact: val_inj. 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