proposition: Lemma unicite_coor_bar_aux : forall (A B C I : PO) (x y x' y' : R), x <> x' :>R \/ y <> y' :>R -> cons 1 I = add_PP (add_PP (cons x A) (cons y B)) (cons (1 + - (x + y)) C) :>PP -> cons 1 I = add_PP (add_PP (cons x' A) (cons y' B)) (cons (1 + - (x' + y')) C) :>PP -> alignes A B C.
proof: Proof. intros. assert (vec C I = add_PP (mult_PP x (vec C A)) (mult_PP y (vec C B))). unfold vec in |- *. rewrite H0; Ringvec. assert (vec C I = add_PP (mult_PP x' (vec C A)) (mult_PP y' (vec C B))). unfold vec in |- *. rewrite H1; Ringvec. assert (add_PP (mult_PP (x + - x') (vec C A)) (mult_PP (y + - y') (vec C B)) = zero). VReplace zero (add_PP (vec C I) (mult_PP (-1) (vec C I))). pattern (vec C I) at 1 in |- *; rewrite H2; rewrite H3; Ringvec. assert (mult_PP (x + - x') (vec C A) = mult_PP (y' + - y) (vec C B)). VReplace (mult_PP (y' + - y) (vec C B)) (add_PP (mult_PP (y' + - y) (vec C B)) zero). rewrite <- H4; Ringvec. elim H; [ intros H6; try clear H; try exact H6 | intros H6; try clear H ]. assert (x + - x' <> 0). contrapose H6. RReplace x' (x' + 0). rewrite <- H; ring. assert (alignes C B A); auto with geo. apply colineaire_alignes with (/ (x + - x') * (y' + - y)). VReplace (mult_PP (/ (x + - x') * (y' + - y)) (vec C B)) (mult_PP (/ (x + - x')) (mult_PP (y' + - y) (vec C B))). rewrite <- H5; Fieldvec (x + - x'). assert (y' + - y <> 0). contrapose H6. RReplace y (y + 0). rewrite <- H; ring. assert (alignes C A B); auto with geo. apply colineaire_alignes with (/ (y' + - y) * (x + - x')). VReplace (mult_PP (/ (y' + - y) * (x + - x')) (vec C A)) (mult_PP (/ (y' + - y)) (mult_PP (x + - x') (vec C A))). rewrite H5; Fieldvec (y' + - y). Qed.