proposition: Theorem translation_reflexion_axe_parallele_commutent : forall A B C D M M1 M2 N1 N2 : PO, A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> M1 = translation A B M -> M2 = reflexion C D M1 -> N1 = reflexion C D M -> N2 = translation A B N1 -> N2 = M2.
proof: Proof. intros A B C D M M1 M2 N1 N2 H H0 H1 H2 H3 H4 H5; try assumption. rewrite H3. cut (vec M M1 = vec A B). intros H100. cut (vec N1 N2 = vec A B). intros H102. cut (vec M M1 = vec N1 N2); intros. elim (paralleles_vecteur (A:=C) (B:=D) (C:=A) (D:=B)); intros; auto with geo. cut (x <> 0); intros. elim (classic (alignes C D M)); intros. generalize (reflexion_axe (A:=C) (B:=D) (M:=M)); intros. cut (N1 = M); intros. rewrite H11 in H6. cut (alignes C D M1); intros. generalize (reflexion_axe (A:=C) (B:=D) (M:=M1)); intros. rewrite <- H13; auto. apply conversion_PP with (a := 1) (b := 1); auto. RingPP2 H6; Ringvec. auto with real. halignes H9 x0. apply colineaire_alignes with (x0 + / x). replace (vec C M1) with (add_PP (vec C M) (vec M M1)). rewrite H12. rewrite <- (translation_vecteur H2). replace (vec A B) with (mult_PP (/ x) (vec C D)). Ringvec. rewrite H7. replace (mult_PP (/ x) (mult_PP x (vec A B))) with (mult_PP (/ x * x) (vec A B)). replace (/ x * x) with 1; auto with real. Ringvec. Ringvec. Ringvec. rewrite H10; auto. elim (existence_projete_orthogonal (A:=C) (B:=D) M); auto; intros K H10. elim existence_representant_vecteur with (A := K) (B := A) (C := B); intros L H11. generalize (reflexion_def (A:=C) (B:=D) (M:=M) (M':=N1) (H:=K)); intros H12. cut (L = milieu M1 N2); intros. generalize (reflexion_axe_orthogonal_segment (A:=C) (B:=D) (M:=M) (M':=N1)); intros. generalize (paralleles_orthogonal (A:=M) (B:=N1) (C:=M1) (D:=N2) (E:=C) (F:=D)); intros. apply reflexion_def2 with L; auto. elim (def_projete_orthogonal2 (A:=C) (B:=D) (C:=M) (H:=K)); auto; intros. apply def_projete_orthogonal; auto. apply (paralleles_alignes1 (A:=A) (B:=B) (C:=C) (D:=D) (E:=K) (F:=L)); auto. replace (vec L M1) with (vec K M); auto. apply egalite_vecteur. rewrite H11; auto with geo. apply milieu_vecteur_double; auto. apply vecteur_milieu. replace (vec M1 N2) with (vec M N1); auto with geo. rewrite H12; auto. cut (2 <> 0); intros; auto with real. replace (mult_PP (/ 2) (mult_PP 2 (vec M K))) with (vec M K); auto. replace (vec M1 L) with (vec M K); auto. apply egalite_vecteur; auto. rewrite H11; auto. Fieldvec 2. red in |- *; intros; apply H0. apply vecteur_nul_conf. rewrite H7; rewrite H8; Ringvec. rewrite H100; auto. symmetry in |- *. apply translation_vecteur; auto. symmetry in |- *. apply translation_vecteur; auto. Qed.