proposition: Theorem composee_rotation_IJ_translation : forall (I J : PO) (a b : R), image_angle (a + b) = image_angle 0 -> exists A : PO, (exists B : PO, (forall M M1 M2 : PO, M1 = rotation I a M -> M2 = rotation J b M1 -> M2 = translation A B M)).
proof: Proof. intros I J a b H; try assumption. discrimine I J. exists J; exists J; intros. generalize (composee_rotations_meme_centre (I:=J) (A:=M) (B:=M1) (C:=M2) (a:=a) (b:=b)); intros. rewrite H3; auto. apply rec_translation_vecteur; auto. rewrite (deux_mes_angle_rotation J M (a:=a + b) (b:=0)); auto. rewrite <- (rotation_angle_nul J M); auto. Ringvec. elim existence_rotation_Ia with (I := J) (M := I) (a := / 2 * b); intros C H7. elim (rotation_def (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto; intros. elim existence_rotation_Ia with (I := I) (M := J) (a := - (/ 2 * a)); intros D H10. elim (rotation_def (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto; intros. cut (I <> D); intros. cut (J <> C); intros. cut (paralleles (droite I D) (droite J C)); intros. elim (existence_projete_orthogonal (A:=J) (B:=C) I). intros K H25; try assumption. generalize (def_projete_orthogonal2 (A:=J) (B:=C) (C:=I) (H:=K)). intros H60. elim H60; auto; intros H61 H62; clear H60. discrimine I K. rewrite <- H9 in H61. exists I; exists I; intros. elim existence_reflexion_AB with (A := I) (B := D) (M := M); [ intros M' H16; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := I) (B := J) (M := M'); [ intros N' H17; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := J) (B := I) (M := M1); [ intros N1 H19; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := J) (B := C) (M := N1); [ intros N2 H21; try clear existence_reflexion_AB | auto ]. generalize (composee_reflexions_axes_secants (A:=J) (B:=I) (C:=C) (M:=M1) (M':=N2) (M1:=N1) (a:=/ 2 * b)); intros H23. generalize (composee_reflexions_axes_secants (A:=I) (B:=D) (C:=J) (M:=M) (M':=N') (M1:=M') (a:=/ 2 * a)); intros H24. cut (M1 = N'); intros. cut (N1 = M'); intros. cut (M2 = N2); intros. rewrite <- H15 in H21; rewrite H14 in H21; auto. generalize (axe_reflexion_droite (A:=J) (B:=C) (C:=I) (M:=M') (M':=M2)); intros. generalize (axe_reflexion_droite (A:=I) (B:=J) (C:=D) (M:=M') (M':=M2)); intros. generalize (axe_reflexion_droite (A:=D) (B:=I) (C:=I) (M:=M') (M':=M2)); intros. rewrite H22; auto with geo. generalize (reflexion_symetrie (A:=I) (B:=D) (M:=M) (M':=M')); intros. rewrite <- H26; auto. apply rec_translation_vecteur; auto. Ringvec. rewrite H20; auto. apply paralleles_alignes3 with (3 := H8); auto. rewrite H23; auto. rewrite H12; auto. apply deux_mes_angle_rotation. replace (/ 2 * b + / 2 * b) with b; auto with real. rewrite H13 in H19. generalize (reflexion_symetrie (A:=I) (B:=J) (M:=M') (M':=N')); intros. rewrite H14; auto. generalize (axe_reflexion_droite (A:=J) (B:=I) (C:=I) (M:=N') (M':=N1)); intros. rewrite H15; auto with geo. rewrite H24; auto. rewrite H11; auto. rewrite <- H9. apply deux_mes_angle_rotation. replace (/ 2 * a + / 2 * a) with a; auto with real. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. replace (- - (/ 2 * a)) with (/ 2 * a); auto. ring. cut (orthogonal (vec I D) (vec I K)); intros. elim existence_representant_vecteur with (A := K) (B := I) (C := D); intros L H28. generalize (egalite_vecteur (A:=K) (B:=L) (C:=I) (D:=D)); intros. cut (K <> L); intros. elim existence_representant_vecteur with (A := K) (B := I) (C := K); intros P H31. exists I; exists P; intros. elim existence_reflexion_AB with (A := I) (B := D) (M := M); [ intros M' H16; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := I) (B := J) (M := M'); [ intros N' H17; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := J) (B := I) (M := M1); [ intros N1 H19; try clear existence_reflexion_AB | auto ]. elim existence_reflexion_AB with (A := J) (B := C) (M := N1); [ intros N2 H21; try clear existence_reflexion_AB | auto ]. generalize (composee_reflexions_axes_secants (A:=J) (B:=I) (C:=C) (M:=M1) (M':=N2) (M1:=N1) (a:=/ 2 * b)); intros H23. generalize (composee_reflexions_axes_secants (A:=I) (B:=D) (C:=J) (M:=M) (M':=N') (M1:=M') (a:=/ 2 * a)); intros H24. cut (M1 = N'); intros. cut (N1 = M'); intros. cut (M2 = N2); intros. generalize (composee_reflexions_axes_paralleles (A:=I) (B:=D) (C:=K) (D:=L) (E:=P) (M:=M) (M':=M2) (M1:=M')); intros. rewrite H26; auto. apply rec_translation_vecteur; auto. apply rec_translation_vecteur; auto. rewrite <- H22 in H21; rewrite H20 in H21; auto. elim (classic (L = J)); intros. rewrite H27. generalize (axe_reflexion_droite (A:=J) (B:=C) (C:=K) (M:=M') (M':=M2)); intros. rewrite <- H29; auto. rewrite H27 in H13; auto. generalize (axe_reflexion_droite (A:=J) (B:=C) (C:=L) (M:=M') (M':=M2)); intros. generalize (axe_reflexion_droite (A:=L) (B:=J) (C:=K) (M:=M') (M':=M2)); intros. rewrite <- H30; auto. apply paralleles_alignes2 with (4 := H8); auto. rewrite H29; auto. apply paralleles_alignes1 with (3 := H28); auto. rewrite H23; auto. rewrite H15; auto. apply deux_mes_angle_rotation. replace (/ 2 * b + / 2 * b) with b; auto with real. rewrite H18 in H19. generalize (reflexion_symetrie (A:=I) (B:=J) (M:=M') (M':=N')); intros. rewrite H20; auto. generalize (axe_reflexion_droite (A:=J) (B:=I) (C:=I) (M:=N') (M':=N1)); intros. rewrite H22; auto with geo. rewrite H24; auto. rewrite H14; auto. apply deux_mes_angle_rotation. replace (/ 2 * a + / 2 * a) with a; auto with real. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. replace (- - (/ 2 * a)) with (/ 2 * a); auto. ring. red in |- *; intros; apply H5. apply vecteur_nul_conf; auto. rewrite <- H28; rewrite <- H13; Ringvec. elim (paralleles_vecteur (A:=I) (B:=D) (C:=J) (D:=C)); auto; intros. replace (vec I D) with (add_PP (mult_PP x (vec J C)) (mult_PP 0 (vec J C))). apply ortho_combinaison_lineaire. apply def_orthogonal2. replace (scalaire (vec J C) (vec I K)) with (- scalaire (vec J C) (vec K I)). rewrite (def_orthogonal (A:=J) (B:=C) (C:=K) (D:=I)); auto. ring. replace (vec I K) with (mult_PP (-1) (vec K I)). Simplscal. Ringvec. auto with geo. rewrite H11; Ringvec. try exact H6. apply droites_paralleles_angle; auto. unfold double_AV in |- *. replace (cons_AV (vec I D) (vec J C)) with (plus (cons_AV (vec I D) (vec I J)) (plus (cons_AV (vec I J) (vec J I)) (cons_AV (vec J I) (vec J C)))); auto. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. rewrite <- H2. rewrite <- angle_plat. repeat rewrite <- add_mes_compatible. replace (- - (/ 2 * a)) with (/ 2 * a); auto. replace (/ 2 * a + (pi + / 2 * b) + (/ 2 * a + (pi + / 2 * b))) with (/ 2 * a + / 2 * a + (/ 2 * b + / 2 * b) + (pi + pi)); auto. replace (/ 2 * a + / 2 * a) with a; auto with real. replace (/ 2 * b + / 2 * b) with b; auto with real. rewrite add_mes_compatible. rewrite H. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (0 + 0) with 0; auto. ring. ring. ring. try exact H0. repeat rewrite Chasles; auto. apply (image_distinct_centre (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto. apply (image_distinct_centre (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto. Qed.