proposition: Lemma unicite_coef_bar : forall (x x0 : R) (A B : PO), A <> B -> 1 + x <> 0 -> 1 + x0 <> 0 -> barycentre (cons 1 A) (cons x B) = barycentre (cons 1 A) (cons x0 B) -> x = x0.
proof: Proof. intros. cut (barycentre (cons (/ (1 + x) * 1) A) (cons (/ (1 + x) * x) B) = barycentre (cons (/ (1 + x0) * 1) A) (cons (/ (1 + x0) * x0) B)); intros. cut (1 + x = 1 + x0); intros. RReplace x (-1 + (1 + x)). rewrite H4. ring. cut (/ (1 + x) = / (1 + x0)); intros. replace (1 + x) with (/ / (1 + x)). rewrite H4. auto with *. auto with *. replace (/ (1 + x)) with (/ (1 + x) * 1). replace (/ (1 + x0)) with (/ (1 + x0) * 1). apply (unicite_coor_bar (k:=/ (1 + x) * 1) (k':=/ (1 + x0) * 1) (A:=A) (B:=B) (I:=barycentre (cons (/ (1 + x) * 1) A) (cons (/ (1 + x) * x) B))); auto. pattern 1 at 1 in |- *. replace 1 with (/ (1 + x) * 1 + / (1 + x) * x). rewrite <- add_PP_barycentre; auto. replace (1 + - (/ (1 + x) * 1)) with (/ (1 + x) * x); auto. auto with *. pattern 1 at 2 in |- *. replace 1 with (/ (1 + x) * (1 + x)); auto. ring. auto with *. replace (/ (1 + x) * 1 + / (1 + x) * x) with 1; auto. auto with *. pattern 1 at 1 in |- *. replace 1 with (/ (1 + x) * (1 + x)); auto. ring. auto with *. replace (/ (1 + x) * 1 + / (1 + x) * x) with (/ (1 + x) * (1 + x)); auto. auto with *. auto with *. rewrite H3. pattern 1 at 1 in |- *. replace 1 with (/ (1 + x0) * 1 + / (1 + x0) * x0). rewrite <- add_PP_barycentre; auto. replace (1 + - (/ (1 + x0) * 1)) with (/ (1 + x0) * x0); auto. pattern 1 at 2 in |- *. replace 1 with (/ (1 + x0) * (1 + x0)); auto. ring. auto with *. replace (/ (1 + x0) * 1 + / (1 + x0) * x0) with 1; auto. auto with *. pattern 1 at 1 in |- *. replace 1 with (/ (1 + x0) * (1 + x0)); auto. ring. auto with *. replace (/ (1 + x0) * 1 + / (1 + x0) * x0) with (/ (1 + x0) * (1 + x0)); auto. auto with *. auto with *. auto with *. ring. rewrite homogene_barycentre. rewrite homogene_barycentre; auto. auto with *. try exact H0. auto with *. Qed.