proposition: Theorem somme_triangle : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> B <> C :>PO -> plus (cons_AV (vec A B) (vec A C)) (plus (cons_AV (vec B C) (vec B A)) (cons_AV (vec C A) (vec C B))) = image_angle pi :>AV.
proof: Proof. intros A B C H H0 H1; try assumption. rewrite <- (angle_oppu_oppv (A:=C) (B:=A) (C:=C) (D:=B)); auto. mesure A B A C. mesure B C B A. mesure A C B C. replace (x + (x0 + x1)) with (x + x1 + x0). repeat rewrite add_mes_compatible. rewrite H4; rewrite H3; rewrite H2; repeat rewrite Chasles; auto. rewrite <- angle_plat; auto. ring. Qed.