proposition: Lemma trianglesSD_angles_egaux : forall A B C A' B' C' :PO, trianglesSD A B C A' B' C' -> cons_AV(vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C').
proof: Proof. intros A B C A' B' C' H. deroule_triangles_semblables. rewrite <- angle_triangle;try auto. rewrite -> H2;rewrite -> H5. apply angle_triangle;auto . Qed.