proposition: Lemma cos_paire : forall x : R, cos (- 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_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 ]. rewrite (def_cos (A:=A) (B:=B) (C:=C) (x:=x)); auto. cut (image_angle (- x) = cons_AV (vec A C) (vec A B)); intros. rewrite (def_cos (A:=A) (B:=C) (C:=B) (x:=- x)); auto. rewrite scalaire_sym; auto. apply mes_oppx; auto with geo. Qed.