proposition: Lemma trigo_Pythagore : forall x : R, Rsqr (cos x) + Rsqr (sin x) = 1.
proof: Proof. unfold Rsqr in |- *; intros. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. 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 ]. elim existence_ROND_AB with (A := A) (B := B); [ intros D H | auto ]. elim H; intros. cut (vec A C = add_PP (mult_PP (cos x) (vec A B)) (mult_PP (sin x) (vec A D))); intros. replace 1 with (scalaire (vec A C) (vec A C)); auto with geo. rewrite H5. Simplscal. elim H4; intros H6 H7; try clear H4; try exact H7. rewrite H7; rewrite H6. rewrite (pisurdeux_scalaire_nul (A:=A) (B:=B) (C:=D)); auto. rewrite scalaire_sym. rewrite (pisurdeux_scalaire_nul (A:=A) (B:=B) (C:=D)); auto. ring. apply coordonnees_cos_sin; auto. Qed.