proposition: Lemma cos_zero : cos 0 = 1.
proof: Proof. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. rewrite (def_cos (A:=A) (B:=B) (C:=B) (x:=0)); auto with geo. rewrite <- angle_nul; auto with geo. Qed.