proposition: Theorem composee_rotation_IJ_rotation : forall (I J : PO) (a b : R), image_angle (a + b) <> image_angle 0 -> ex (fun K : PO => forall M M1 M2 : PO, M1 = rotation I a M -> M2 = rotation J b M1 -> M2 = rotation K (a + b) M).
proof: Proof. intros I J a b H; try assumption. discrimine I J. exists I; intros. generalize (composee_rotations_meme_centre (I:=J) (A:=M) (B:=M1) (C:=M2) (a:=a) (b:=b)); intros. rewrite H0; rewrite H3; auto. elim existence_rotation_Ia with (I := J) (M := I) (a := / 2 * b); intros C H7. elim existence_rotation_Ia with (I := I) (M := J) (a := - (/ 2 * a)); intros D H10. cut (I <> D); intros. cut (J <> C); intros. generalize (position_relative_droites_coplanaires (A:=I) (B:=D) (C:=J) (D:=C)); intros. elim H3; intros. elim def_concours2 with (A := I) (B := D) (C := J) (D := C); [ intros K H27; try clear def_concours2; try exact H27 | auto | auto | auto ]. elim H27; intros H28 H29; try clear H27; try exact H29. exists K; 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. elim (classic (I = K)); intros. cut (J <> K); intros. rewrite <- H12 in H29; rewrite <- H12. elim (rotation_def (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto; intros. cut (image_angle b = image_angle 0); intros. cut (M2 = M1); intros. rewrite H20; rewrite H5. apply deux_mes_angle_rotation. rewrite add_mes_compatible. rewrite H18; rewrite <- add_mes_compatible. replace (a + 0) with a; auto. ring. rewrite H6. pattern M1 at 2 in |- *. rewrite (rotation_angle_nul J M1). apply deux_mes_angle_rotation; auto. replace b with (/ 2 * b + / 2 * b); auto with real. generalize (angle_alignes (A:=J) (B:=I) (C:=C)); intros H22; rewrite <- H22; auto with geo. unfold double_AV in |- *. rewrite <- H15. rewrite add_mes_compatible; auto. red in |- *; intros; apply H0. rewrite H12; rewrite H13; auto. elim (classic (J = K)); intros. rewrite <- H13 in H28; rewrite <- H13. elim (rotation_def (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto; intros. cut (image_angle a = image_angle 0); intros. cut (M1 = M); intros. rewrite <- H20; rewrite H6. apply deux_mes_angle_rotation. rewrite add_mes_compatible. rewrite H18; rewrite <- add_mes_compatible. replace (0 + b) with b; try ring; auto. rewrite (rotation_angle_nul I M). rewrite H5. apply deux_mes_angle_rotation; auto. replace a with (/ 2 * a + / 2 * a); auto with real. generalize (angle_alignes (A:=I) (B:=D) (C:=J)); intros H22; rewrite <- H22; auto. unfold double_AV in |- *. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. replace (- - (/ 2 * a)) with (/ 2 * a); auto. rewrite add_mes_compatible; auto. ring. mesure I K J K. cut (plus (cons_AV (vec I K) (vec J K)) (cons_AV (vec I K) (vec J K)) = image_angle (a + b)); intros. generalize (composee_reflexions_axes_secants (A:=K) (B:=I) (C:=J) (M:=M) (M':=M2) (M1:=M') (a:=x)); intros. rewrite H18; auto. apply deux_mes_angle_rotation. rewrite add_mes_compatible. rewrite H14; rewrite H15; auto. rewrite angle_oppu_oppv; auto. generalize (axe_reflexion_droite (A:=I) (B:=D) (C:=K) (M:=M) (M':=M')); intros. rewrite H20; auto. generalize (axe_reflexion_droite (A:=J) (B:=C) (C:=K) (M:=N1) (M':=N2)); intros. rewrite H11; rewrite H20; auto; rewrite H9; auto. replace (plus (cons_AV (vec I K) (vec J K)) (cons_AV (vec I K) (vec J K))) with (double_AV (cons_AV (vec I K) (vec J K))); auto. generalize (alignement_et_angles (A:=I) (B:=D) (C:=K) (D:=J) (E:=C) (F:=K)); intros. rewrite <- H15; 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 <- angle_plat; auto. elim (rotation_def (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto; intros. elim (rotation_def (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto; intros. rewrite <- H25. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. repeat rewrite <- add_mes_compatible. replace (- - (/ 2 * a)) with (/ 2 * a). replace (/ 2 * a + (pi + / 2 * b) + (/ 2 * a + (pi + / 2 * b))) with (/ 2 * a + / 2 * a + (/ 2 * b + / 2 * b) + (pi + pi)). replace (/ 2 * a + / 2 * a) with a; auto with real. replace (/ 2 * b + / 2 * b) with b; auto with real. replace (pi + pi) with deuxpi; auto. rewrite add_mes_compatible. rewrite pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (a + b + 0) with (a + b); auto. ring. ring. ring. repeat rewrite Chasles; auto. rewrite H6; rewrite H23; auto. apply deux_mes_angle_rotation. replace (/ 2 * b + / 2 * b) with b; auto with real. elim (rotation_def (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto; intros. rewrite <- H8 in H17. generalize (reflexion_symetrie (A:=I) (B:=J) (M:=M') (M':=M1)); intros. rewrite H9; auto. generalize (axe_reflexion_droite (A:=J) (B:=I) (C:=I) (M:=M1) (M':=N1)); intros. rewrite H11; auto with geo. rewrite H5; rewrite H24; auto. apply deux_mes_angle_rotation. replace (/ 2 * a + / 2 * a) with a; auto with real. elim (rotation_def (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto; intros. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. replace (- - (/ 2 * a)) with (/ 2 * a); auto. ring. absurd (paralleles (droite J C) (droite I D)); auto with geo. cut (double_AV (cons_AV (vec I D) (vec J C)) = image_angle (a + b)); intros. apply angle_non_paralleles; auto. red in |- *; intros; apply H. rewrite <- H6; auto. rewrite add_mes_compatible; 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 <- angle_plat; auto. elim (rotation_def (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto; intros. elim (rotation_def (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto; intros. rewrite <- H9. rewrite <- (mes_oppx (A:=I) (B:=J) (C:=I) (D:=D) (x:=- (/ 2 * a))); auto. repeat rewrite <- add_mes_compatible. replace (- - (/ 2 * a)) with (/ 2 * a). replace (/ 2 * a + (pi + / 2 * b) + (/ 2 * a + (pi + / 2 * b))) with (/ 2 * a + / 2 * a + (/ 2 * b + / 2 * b) + (pi + pi)). replace (/ 2 * a + / 2 * a) with a; auto with real. replace (/ 2 * b + / 2 * b) with b; auto with real. replace (pi + pi) with deuxpi; auto. rewrite add_mes_compatible. rewrite pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (a + b + 0) with (a + b); auto. ring. ring. ring. repeat rewrite Chasles; auto. apply (image_distinct_centre (I:=I) (A:=J) (B:=D) (a:=- (/ 2 * a))); auto. apply (image_distinct_centre (I:=J) (A:=I) (B:=C) (a:=/ 2 * b)); auto. apply geometrie_plane; 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.