proposition: Lemma sin_pisurdeux : sin pisurdeux = 1.
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 H3 H4; try clear H2; try exact H4. rewrite (def_sin (A:=A) (B:=B) (C:=D) (D:=D) (x:=pisurdeux)); auto with geo. Qed.