proposition: Lemma Sin_opp : forall A B C D : PO, A <> B -> C <> D -> Sin (cons_AV (vec C D) (vec A B)) = - Sin (cons_AV (vec A B) (vec C D)).
proof: Proof. intros. elim (existence_representant_vecteur A C D); intros E; intros. rewrite <- H1. cut (A <> E); intros. mesure A B A E. rewrite H3. generalize (mes_oppx (A:=A) (B:=B) (C:=A) (D:=E) (x:=x)); auto; intros. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=E) (x:=x)); auto. rewrite <- (egalite_sin_Sin (A:=A) (B:=E) (C:=B) (x:=- x)); auto. rewrite sin_impaire; auto. apply distinct_egalite_vecteur with (A := C) (B := D); auto. Qed.