proposition: Lemma Sin_angles_alignes : forall A B C : PO, A <> B -> A <> C -> alignes A B C -> Sin (cons_AV (vec A B) (vec A C)) = 0.
proof: Proof. intros. deroule_representant_unitaire A B D. deroule_representant_unitaire A C E. rewrite angles_representants_unitaires; auto. elim alignes_representant_unitaire with (A := A) (B := B) (C := C); [ intros H12 | intros H12 | auto | auto | auto ]. rewrite H12; rewrite <- H7. rewrite <- (egalite_sin_Sin (A:=A) (B:=E) (C:=E) (x:=0)); auto with geo. rewrite H12; rewrite <- H2. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := D) (k := -1); [ intros F H13; try clear existence_representant_mult_vecteur; try exact H13 ]. rewrite <- H13. rewrite <- (egalite_sin_Sin (A:=A) (B:=D) (C:=F) (x:=pi)); auto with geo. apply distinct_produit_vecteur with (3 := H13); auto with real. rewrite H13. VReplace (mult_PP (-1) (vec A D)) (vec D A); auto with geo. Qed.