proposition: Lemma pisurdeux_plus_x : forall x : R, cos (pisurdeux + x) = - sin x /\ sin (pisurdeux + x) = cos x.
proof: Proof. intros. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. elim existence_ROND_AB with (A := A) (B := B); [ intros D H10 | auto ]. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := pisurdeux + x); [ intros C H; elim H; intros H1 H2; try clear H; try exact H2 | auto ]. elim H10; intros. elim H3; intros H6 H7; try clear H3; try exact H7. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := -1); intros E H4. cut (image_angle x = cons_AV (vec A D) (vec A C)); intros. generalize (coordonnees_cos_sin (x:=pisurdeux + x) (O:=A) (I:=B) (J:=D) (M:=C)); intros. generalize (coordonnees_cos_sin (x:=x) (O:=A) (I:=D) (J:=E) (M:=C)); intros. cut (vec A C = add_PP (mult_PP (- sin x) (vec A B)) (mult_PP (cos x) (vec A D))); intros. apply unicite_coordonnees with (3 := H9); auto with geo. rewrite H8; auto. rewrite H4. unfold vec in |- *; RingPP. apply ROND_new with B; auto. replace x with (- pisurdeux + (pisurdeux + x)); try ring. replace (cons_AV (vec A D) (vec A C)) with (plus (cons_AV (vec A D) (vec A B)) (cons_AV (vec A B) (vec A C))). replace (cons_AV (vec A D) (vec A B)) with (image_angle (- pisurdeux)). rewrite <- H2. apply add_mes_compatible. apply mes_oppx; auto with geo. apply Chasles; auto with geo. Qed.