proposition: Lemma sin_periodique : forall x : R, sin (x + deuxpi) = sin 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 := x); [ intros C H; elim H; intros H1 H2; try clear H; try exact H2 | auto ]. rewrite (def_sin (A:=A) (B:=B) (C:=C) (D:=D) (x:=x)); auto. cut (image_angle (x + deuxpi) = cons_AV (vec A B) (vec A C)); intros. rewrite (def_sin (A:=A) (B:=B) (C:=C) (D:=D) (x:=x + deuxpi)); auto. apply mesure_mod_deuxpi; auto with geo. Qed.