proposition: Theorem composee_reflexions_axes_paralleles : forall A B C D E M M' M1 : PO, A <> B -> A <> C -> orthogonal (vec A B) (vec A C) -> D = translation A B C -> E = translation A C C -> M1 = reflexion A B M -> M' = reflexion C D M1 -> M' = translation A E M.
proof: Proof. intros A B C D E M M' M1 H11 H0 H6 H2 H3 H4 H5; try assumption. generalize (translation_vecteur (I:=A) (J:=C) (A:=C) (A':=E)); intros H21. generalize (translation_vecteur (I:=A) (J:=B) (A:=C) (A':=D)); intros H22. cut (C <> D). intros H7. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H8; try clear existence_projete_orthogonal; try exact H8 | auto ]. elim existence_projete_orthogonal with (A := C) (B := D) (C := M1); [ intros H1 H12; try clear existence_projete_orthogonal | auto ]. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros | auto | auto ]. elim def_projete_orthogonal2 with (A := C) (B := D) (C := M1) (H := H1); [ intros | auto | auto ]. apply rec_translation_vecteur. generalize (reflexion_projete_orthogonal_milieu (A:=A) (B:=B) (M:=M) (M':=M1) (H:=H)); intros. generalize (reflexion_projete_orthogonal_milieu (A:=C) (B:=D) (M:=M1) (M':=M') (H:=H1)); intros. replace (vec M M') with (add_PP (vec M M1) (vec M1 M')). rewrite (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M1) (H:=H)); auto. rewrite (reflexion_def (A:=C) (B:=D) (M:=M1) (M':=M') (H:=H1)); auto. rewrite (milieu_vecteur (A:=M) (B:=M1) (M:=H)); auto. replace (add_PP (mult_PP 2 (vec H M1)) (mult_PP 2 (vec M1 H1))) with (mult_PP 2 (add_PP (vec H M1) (vec M1 H1))). replace (add_PP (vec H M1) (vec M1 H1)) with (vec H H1). cut (vec H H1 = vec A C); intros. rewrite H17. generalize (translation_vecteur (I:=A) (J:=C) (A:=C) (A':=E)); intros. replace (vec A E) with (add_PP (vec A C) (vec C E)). rewrite H18; auto. Ringvec. Ringvec. generalize (triangle_rectangle_repere (O:=A) (I:=B) (J:=C)); intros. halignes H9 k. halignes H13 k0. elim (classic (k = 0)); intros. cut (A = H); intros. generalize (translation_bipoint (I:=A) (J:=B) (A:=A) (A':=B) (B:=C) (B':=D)); intros. cut (B <> D); intros. cut (orthogonal (vec B A) (vec B D)); intros. generalize (triangle_rectangle_repere (O:=B) (I:=A) (J:=D)); intros. rewrite H24; auto with geo. elim orthogonal_paralleles with (A := B) (B := A) (C := D) (E := H) (F := H1); [ intros k1 H28; try clear orthogonal_paralleles | auto | auto | auto | auto ]. rewrite (couple_colineaires_parallelogramme (A:=B) (B:=H) (C:=D) (D:=H1) (k:=1 + - k0) (k':=k1)); auto. unfold not in |- *; intros; apply H11. rewrite H29; rewrite H23; auto. rewrite <- H23. auto with geo. replace (vec D H1) with (add_PP (mult_PP (-1) (vec C D)) (vec C H1)). rewrite H19. rewrite <- H23. rewrite <- H22; auto. Ringvec. Ringvec. cut (orthogonal (vec H H1) (vec A B)); intros; auto with geo. replace (vec H H1) with (add_PP (vec H M) (vec M H1)). apply ortho_somme; auto with geo. replace (vec M H1) with (add_PP (mult_PP 1 (vec M M1)) (mult_PP (-1) (vec H1 M1))). Simplortho. replace (vec M M1) with (add_PP (mult_PP (-1) (vec H M)) (mult_PP 1 (vec H M1))). Simplortho. rewrite <- (milieu_vecteur (A:=M) (B:=M1) (M:=H)); auto with geo. Ringvec. rewrite H22; auto with geo. Ringvec. Ringvec. rewrite <- H24; auto with geo. unfold not in |- *; intros; apply H0. cut (vec A C = vec B D); auto with geo; intros. rewrite H25 in H26. apply conversion_PP with (a := 1) (b := 1); auto. RingPP2 H26. Ringvec. discrR. apply conversion_PP with (a := 1) (b := 1); auto. RingPP2 H18. rewrite H20. Ringvec. discrR. elim orthogonal_paralleles with (A := A) (B := B) (C := C) (E := H) (F := H1); [ intros k1 H23; try clear orthogonal_paralleles; try exact H23 | auto | auto | auto | auto ]. rewrite <- H22 in H19; auto. cut (vec A B = mult_PP (/ k) (vec A H)); intros; auto with geo. rewrite H24 in H19. rewrite (couple_colineaires_parallelogramme (A:=A) (B:=H) (C:=C) (D:=H1) (k:=k0 * / k) (k':=k1)); auto. unfold not in |- *; intros; apply H20. rewrite <- H25 in H18; auto. elim produit_vecteur_nul with (a := k) (A := A) (B := B); [ intros H26; try clear produit_vecteur_nul; try exact H26 | intros H26; try clear produit_vecteur_nul | try clear produit_vecteur_nul ]. absurd (A = B); auto. rewrite <- H18; Ringvec. apply alignes_non_alignes_trans with B; auto with geo. apply distinct_produit_vecteur with (3 := H18); auto. rewrite H19; Ringvec. rewrite H18. Fieldvec k. cut (vec A H1 = add_PP (mult_PP k0 (vec A B)) (mult_PP 1 (vec A C))); intros. replace (vec H H1) with (add_PP (vec H M) (vec M H1)). Simplortho. replace (vec M H1) with (add_PP (mult_PP 1 (vec M M1)) (mult_PP (-1) (vec H1 M1))). Simplortho. replace (vec M M1) with (add_PP (mult_PP (-1) (vec H M)) (mult_PP 1 (vec H M1))). Simplortho. rewrite <- (milieu_vecteur (A:=M) (B:=M1) (M:=H)); auto with geo. Ringvec. rewrite H22; auto with geo. Ringvec. Ringvec. replace (vec A H1) with (add_PP (vec A C) (vec C H1)). rewrite H19; rewrite H22; auto. Ringvec. Ringvec. Ringvec. Ringvec. Ringvec. unfold not in |- *; intros; apply H11. cut (vec A B = vec C D); auto; intros. rewrite H in H1. apply conversion_PP with (a := 1) (b := 1); auto. RingPP2 H1. Ringvec. Qed.