proposition: Lemma cos_deux_mes : forall x y : R, image_angle x = image_angle y -> cos x = cos y.
proof: Proof. intros. elim existence_AB_unitaire; intros A H1; elim H1; intros B H0; try clear H1. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := x); [ intros C H1; elim H1; intros; try clear H1 | auto ]. rewrite (def_cos (A:=A) (B:=B) (C:=C) (x:=x)); auto. rewrite (def_cos (A:=A) (B:=B) (C:=C) (x:=y)); auto. rewrite <- H3; auto. Qed.