proposition: Lemma sin_pi : sin pi = 0.
proof: Proof. 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 H | auto ]. elim H; intros. elim H2; intros H4 H5; try clear H2; try exact H4. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := -1); intros E H3. rewrite (def_sin (A:=A) (B:=B) (C:=E) (D:=D) (x:=pi)); auto. rewrite H3. cut (scalaire (vec A B) (vec A D) = 0); auto with geo; intros. Simplscal; rewrite H2; ring. cut (scalaire (vec A E) (vec A E) = 1); auto with geo; intros. rewrite H3. Simplscal; rewrite H4; ring. replace (vec A E) with (vec B A). rewrite <- angle_plat; auto with geo. rewrite H3. Ringvec. Qed.