proposition: Theorem composee_translation_rotation : forall (I A B : PO) (a : R), image_angle a <> image_angle 0 -> exists J : PO, (forall M M1 M2 : PO, M1 = translation A B M -> M2 = rotation I a M1 -> M2 = rotation J a M).
proof: Proof. intros I A B a H50; try assumption. elim (classic (A = B)); intros H2. exists I; intros. generalize (translation_vecteur (I:=A) (J:=B) (A:=M) (A':=M1)); intros. cut (M1 = M); intros. rewrite H3 in H0; auto. symmetry in |- *. apply vecteur_nul_conf. rewrite <- H1; auto. rewrite <- H2; Ringvec. elim existence_representant_vecteur with (A := I) (B := milieu A B) (C := A); intros D H3; try clear existence_representant_vecteur; try exact H3. cut (vec A B = mult_PP 2 (mult_PP (/ 2) (vec A B))); intros. cut (I <> D); intros. elim existence_rotation_Ia with (I := I) (M := D) (a := pisurdeux); intros C H7. cut (I <> C); auto; intros. cut (orthogonal (vec I C) (vec I D)); intros. elim existence_representant_vecteur with (A := C) (B := I) (C := D); intros E H10; try clear existence_representant_vecteur; try exact H10. generalize (egalite_vecteur (A:=C) (B:=E) (C:=I) (D:=D)). intros H33. elim existence_representant_vecteur with (A := D) (B := A) (C := B); intros F H11; try clear existence_representant_vecteur; try exact H11. cut (D <> E); intros. cut (paralleles (droite I C) (droite D E)); intros. elim existence_rotation_Ia with (I := I) (M := C) (a := / 2 * a); intros G H18. cut (I <> G); intros. generalize (rotation_def (I:=I) (A:=C) (B:=G) (a:=/ 2 * a)); intros. generalize (position_relative_droites_coplanaires (A:=D) (B:=E) (C:=I) (D:=G)); intros. elim H12; intros; auto with geo. elim def_concours2 with (A := D) (B := E) (C := I) (D := G); [ intros J H27; try clear def_concours2; try exact H27 | auto | auto | auto ]. elim H27; intros H28 H29; try clear H27; try exact H29. cut (J <> I); intros. exists J; intros. generalize (translation_vecteur (I:=A) (J:=B) (A:=M) (A':=M1)); intros. elim existence_reflexion_AB with (A := D) (B := E) (M := M); [ intros M' H23; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := I) (B := C) (M := M'); [ intros N H24; try clear existence_reflexion_AB | auto ]. generalize (composee_reflexions_axes_paralleles (A:=D) (B:=E) (C:=I) (D:=C) (E:=F) (M:=M) (M':=N) (M1:=M')); intros. cut (N = translation D F M); intros. cut (M1 = N); intros. elim existence_reflexion_AB with (A := I) (B := C) (M := M1); [ intros N' H31; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := I) (B := G) (M := N'); [ intros N1 H32; try clear existence_reflexion_AB | auto ]. generalize (reflexion_symetrie (A:=I) (B:=C) (M:=M') (M':=N)); intros. rewrite H21 in H31. cut (N' = M'); intros. generalize (composee_reflexions_axes_secants (A:=I) (B:=C) (C:=G) (M:=N) (M':=N1) (M1:=N') (a:=/ 2 * a)); intros. rewrite H16. rewrite H21. replace a with (/ 2 * a + / 2 * a); auto. rewrite <- H26; auto. elim H9; intros. cut (D <> J \/ E <> J); intros. elim H34; [ intros H35; try clear H34 | intros H35; try clear H34; try exact H35 ]. mesure J D J I. cut (double_AV (cons_AV (vec J D) (vec J I)) = image_angle a); intros. generalize (axe_reflexion_droite (A:=D) (B:=E) (C:=J) (M:=M) (M':=M')); intros. generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1)); intros. generalize (composee_reflexions_axes_secants (A:=J) (B:=D) (C:=I) (M:=M) (M':=N1) (M1:=M') (a:=x)); intros. rewrite H39; auto. apply deux_mes_angle_rotation. rewrite add_mes_compatible. unfold double_AV in H36. rewrite H34; rewrite H36. replace (/ 2 * a + / 2 * a) with a; auto with real. apply (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1)); auto. rewrite H32; rewrite H25; auto. rewrite (angles_et_paralleles (A:=J) (B:=D) (C:=J) (D:=I) (E:=I) (F:=C) (G:=I) (I:=G)). unfold double_AV in |- *; rewrite <- H30. rewrite <- add_mes_compatible. replace (/ 2 * a + / 2 * a) with a; auto with real. auto. red in |- *; intros. rewrite H36 in H28. absurd (alignes D E I); auto. auto. auto. generalize (alignes_paralleles (A:=D) (B:=E) (C:=J)); intros. apply paralleles_trans with (C := D) (D := E); auto with geo. apply paralleles_trans with (C := D) (D := J); auto with geo. generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros. apply paralleles_trans with (C := I) (D := J); auto with geo. mesure J E J I. cut (plus (cons_AV (vec J E) (vec J I)) (cons_AV (vec J E) (vec J I)) = image_angle a); intros. generalize (axe_reflexion_droite (A:=E) (B:=D) (C:=J) (M:=M) (M':=M')); intros. generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1)); intros. generalize (composee_reflexions_axes_secants (A:=J) (B:=E) (C:=I) (M:=M) (M':=N1) (M1:=M') (a:=x)); intros. rewrite H39; auto. apply deux_mes_angle_rotation. rewrite add_mes_compatible. unfold double_AV in H36. rewrite H34; rewrite H36. replace (/ 2 * a + / 2 * a) with a; auto with real. apply (axe_reflexion_droite (A:=E) (B:=D) (C:=J) (M:=M) (M':=M')); auto with geo. apply (axe_reflexion_droite (A:=D) (B:=E) (C:=E) (M:=M) (M':=M')); auto with geo. apply (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1)); auto with geo. rewrite H32; rewrite H25; auto. replace (plus (cons_AV (vec J E) (vec J I)) (cons_AV (vec J E) (vec J I))) with (double_AV (cons_AV (vec J E) (vec J I))); auto. rewrite (angles_et_paralleles (A:=J) (B:=E) (C:=J) (D:=I) (E:=I) (F:=C) (G:=I) (I:=G)). unfold double_AV in |- *. rewrite <- H30. rewrite <- add_mes_compatible. replace (/ 2 * a + / 2 * a) with a; auto with real. auto. auto. auto. auto. generalize (alignes_paralleles (A:=E) (B:=D) (C:=J)); intros. apply paralleles_trans with (C := D) (D := E); auto with geo. apply paralleles_trans with (C := E) (D := D); auto with geo. apply paralleles_trans with (C := E) (D := J); auto with geo. generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros. apply paralleles_trans with (C := I) (D := J); auto with geo. apply not_and_or. red in |- *; intros. elim H34; intros. apply H5. rewrite H36; rewrite H35; auto. auto. auto. elim H9; intros; auto with real. auto with real. rewrite H22; auto. rewrite H20. apply rec_translation_vecteur. rewrite <- H17; auto. apply H19; auto. replace (vec D E) with (vec I C). apply ortho_sym; auto with geo. apply egalite_vecteur; auto with geo. apply rec_translation_vecteur. apply egalite_vecteur; auto with geo. replace (vec D I) with (mult_PP (-1) (vec I D)). rewrite <- H10; Ringvec. Ringvec. apply rec_translation_vecteur. replace (vec D I) with (mult_PP (-1) (vec I D)). replace (vec I F) with (add_PP (vec I D) (vec D F)). rewrite H11; rewrite H3; auto. rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto. Ringvec. Ringvec. Ringvec. red in |- *; intros. rewrite H14 in H28. absurd (alignes D E I); auto. apply orthogonal_non_alignes; auto. replace (vec D E) with (vec I C); auto with geo. absurd (paralleles (droite D E) (droite I G)); auto with geo. generalize (angle_non_paralleles (A:=I) (B:=C) (C:=I) (D:=G)); intros. apply non_paralleles_trans with (A := I) (B := C); auto with geo. red in |- *; intros. apply H14; auto with geo. elim H9; auto; intros. unfold double_AV in |- *; rewrite <- H17. rewrite <- add_mes_compatible. replace (/ 2 * a + / 2 * a) with a; auto with real. apply image_distinct_centre with (2 := H18); auto with geo. apply (colineaires_paralleles (k:=1) (A:=I) (B:=C) (C:=D) (D:=E)); auto. replace (vec D E) with (vec I C); auto with geo. Ringvec. red in |- *; intros; apply H1. symmetry in |- *. apply vecteur_nul_conf; auto. rewrite H33; auto. rewrite H5; Ringvec. elim (rotation_def (I:=I) (A:=D) (B:=C) (a:=pisurdeux)); auto with geo; intros. apply image_distinct_centre with (2 := H7); auto. red in |- *; intros; apply H2. apply vecteur_nul_conf; auto. rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto. replace (vec A (milieu A B)) with (mult_PP (-1) (vec (milieu A B) A)). rewrite <- H3; rewrite H0; auto. Ringvec. Ringvec. cut (2 <> 0); intros; auto with real. Fieldvec 2. Qed.