proposition: Lemma existence_rotation_Ia : forall (I M : PO) (a : R), exists M' : PO, M' = rotation I a M.
proof: Proof. intros. elim (classic (M = I)); intros. exists I. rewrite H; rewrite <- rotation_def_centre; auto. elim existence_representant_unitaire with (A := I) (B := M); [ intros; try clear existence_representant_unitaire | auto ]. cut (I <> x); intros. generalize (existence_representant_angle (A:=I) (B:=x) I a); intros. elim H2; [ intros C H3; elim H3; intros H4 H5; try clear H3 H2; try exact H5 | idtac ]. cut (I <> C); intros. generalize (distance_vecteur (A:=I) (B:=M)); intros. elim existence_representant_mult_vecteur with (A := I) (B := I) (C := C) (k := distance I M); intros D H6; try clear existence_representant_mult_vecteur; try exact H6. cut (I <> D); intros. exists D. apply rotation_def2; auto. apply resolution; auto with geo. repeat rewrite <- carre_scalaire_distance. rewrite H6; rewrite H3; auto. rewrite <- H0. Simplscal. elim def_representant_unitaire2 with (A := I) (B := M) (C := x); [ intros; elim H9; intros H22 H23; rewrite H22; try discrR | auto | auto ]. rewrite carre_scalaire_distance. rewrite H4. ring. rewrite angles_representants_unitaires; auto. replace (representant_unitaire (vec I D)) with (vec I C). rewrite <- H0; auto. apply def_representant_unitaire; auto with geo. cut (distance I M <> 0); intros; auto with geo. apply colineaire_alignes with (/ distance I M); auto. rewrite H6. Fieldvec (distance I M). rewrite H6. replace (scalaire (mult_PP (distance I M) (vec I C)) (vec I C)) with (distance I M * scalaire (vec I C) (vec I C)). apply Rmult_pos; auto with geo. Simplscal. apply distinct_produit_vecteur with (3 := H6); auto with geo. auto with geo. elim def_representant_unitaire2 with (A := I) (B := M) (C := x); [ intros; elim H4; intros H22 H23; try discrR | auto | auto ]. auto with geo. apply distance_non_nulle. elim def_representant_unitaire2 with (A := I) (B := M) (C := x); [ intros; elim H2; intros H22 H23; rewrite H22; try discrR | auto | auto ]. Qed.