proposition: Lemma trianglesSD_angles_cotes : forall A B C M N P :PO, trianglesSD A B C M N P-> exists x:R, cons_AV (vec M N)(vec A B) =image_angle x /\ cons_AV (vec N P)(vec B C) =image_angle x /\ cons_AV (vec P M)(vec C A) =image_angle x.
proof: Proof. intros A B C M N P H. expand_triangles_semblables. elim (tout_angle_a_une_mesure (A:=N) (B:=P) (C:=B) (D:=C)); auto with geo. intros x H13. exists x;repeat split;auto. rewrite <-(@Chasles M N P N A B);auto. rewrite <-(@Chasles P N C B A B);auto. rewrite (@plus_commutative (cons_AV (vec P N)(vec C B)) (cons_AV(vec C B)(vec A B))). rewrite plus_associative. rewrite (@angle_oppu_oppv B C B A);auto. rewrite H2. rewrite <-(@angle_oppu_oppv N P N M);auto. rewrite Chasles;auto. rewrite (@angle_oppu_oppv N P B C);auto. rewrite <-H13. rewrite <-angle_nul;auto. rewrite plus_commutative. rewrite plus_angle_zero;auto. rewrite <-(@Chasles P M P N C A );auto. rewrite <-(@Chasles P N C B C A);auto. rewrite (@plus_commutative (cons_AV (vec P N)(vec C B)) (cons_AV(vec C B)(vec C A))). rewrite plus_associative. rewrite <-H5. rewrite Chasles;auto. rewrite (@angle_oppu_oppv N P B C);auto. rewrite <-H13. rewrite <-angle_nul;auto. rewrite plus_commutative. rewrite plus_angle_zero;auto. Qed.