proposition: Lemma cos_pi : cos pi = -1.
proof: Proof. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := -1); intros D H1. cut (scalaire (vec A D) (vec A D) = 1); intros. rewrite (def_cos (A:=A) (B:=B) (C:=D) (x:=pi)); auto with geo. rewrite H1. Simplscal; rewrite carre_scalaire_distance; rewrite H0; ring. replace (vec A D) with (vec B A). rewrite <- angle_plat; auto with geo. rewrite H1. Ringvec. rewrite H1. Simplscal; rewrite carre_scalaire_distance; rewrite H0; ring. Qed.