proposition: Lemma trianglesSI_angles_egaux: forall A B C A' B' C' :PO, trianglesSI A B C A' B' C' -> cons_AV (vec A B)(vec A C) = cons_AV (vec A' C') (vec A' B').
proof: Proof. intros A B C A' B' C' H. deroule_triangles_semblables. rewrite <- angle_triangle;try auto. rewrite -> H2;rewrite -> H5. rewrite <-somme_triangle with A' C' B'; try auto. mesure A' C' A' B'. mesure B' A' B' C'. mesure C' B' C' A'. repeat rewrite <- mes_opp. repeat rewrite <-add_mes_compatible. replace (x+(x1+x0) + -(x0+x1)) with x; [auto|ring]. Qed.