proposition: Lemma sin_cos_pisurdeux_moins_x : forall x : R, sin x = cos (pisurdeux + - x).
proof: Proof. intros. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := x); [ intros C H; elim H; intros H1 H2; try clear H; try exact H2 | auto ]. elim existence_ROND_AB with (A := A) (B := B); [ intros D H; try exact H | auto ]. rewrite (def_sin (A:=A) (B:=B) (C:=C) (D:=D) (x:=x)); auto. cut (image_angle (- x) = cons_AV (vec A C) (vec A B)); intros. replace (pisurdeux + - x) with (- x + pisurdeux); try ring. elim H; intros. elim H5; intros H6 H7; try clear H5; try exact H7. rewrite (def_cos (A:=A) (B:=C) (C:=D) (x:=- x + pisurdeux)); auto with geo. rewrite add_mes_compatible. rewrite H3; rewrite H4; rewrite Chasles; auto with geo. apply mes_oppx; auto with geo. Qed.