proposition: Lemma angle_triangle : forall A B C : PO, A <> B -> A <> C -> B <> C -> plus (image_angle pi) (opp (plus (cons_AV (vec A B) (vec A C)) (cons_AV (vec B C) (vec B A)))) = cons_AV (vec C A) (vec C B).
proof: Proof. intros. rewrite <- (somme_triangle (A:=A) (B:=B) (C:=C)); auto. rewrite opp_plus_plus_opp; auto. mesure B C B A. mesure C A C B. mesure A B A C. replace (x1 + (x + x0) + (- x1 + - x)) with x0; auto. ring. Qed.