proposition: Theorem composee_reflexions_axes_secants : forall (A B C M M' M1 : PO) (a : R), A <> B -> A <> C -> image_angle a = cons_AV (vec A B) (vec A C) -> M1 = reflexion A B M -> M' = reflexion A C M1 -> M' = rotation A (a + a) M.
proof: Proof. intros A B C M M' M1 a H H0 H1 H2 H3; try assumption. elim (classic (A = M)). intros H5; try assumption. rewrite <- H5 in H2. rewrite H2 in H3. rewrite <- (reflexion_axe (A:=A) (B:=B) (M:=A)) in H3; auto with geo. rewrite <- (reflexion_axe (A:=A) (B:=C) (M:=A)) in H3; auto with geo. rewrite H3; rewrite <- H5. apply rotation_def_centre. elim (classic (alignes A B M)); intros. cut (M1 = M); intros; auto. rewrite H6 in H3. elim (classic (alignes A C M)); intros. cut (alignes A B C); intros. cut (M' = M); intros. rewrite H9. pattern M at 1 in |- *. rewrite (rotation_angle_nul A M). apply deux_mes_angle_rotation. symmetry in |- *. replace (image_angle (a + a)) with (double_AV (cons_AV (vec A B) (vec A C))). apply angle_alignes; auto. rewrite add_mes_compatible. rewrite H1; auto. rewrite H3; symmetry in |- *. apply reflexion_axe with (2 := H7); auto. cut (alignes A M C); auto with geo; intros. apply alignes_trans with M; auto with geo. generalize (axe_reflexion_bissectrice (A:=A) (B:=C) (M:=M) (M':=M')); intros. apply rotation_def2; auto. generalize (reflexion_mediatrice (A:=A) (B:=C) (M:=M) (M':=M')); intros. elim H9; intros; auto. cut (cons_AV (vec A M) (vec A B) = cons_AV (vec A B) (vec A M)); intros. replace (cons_AV (vec A M) (vec A M')) with (plus (plus (cons_AV (vec A M) (vec A B)) (cons_AV (vec A B) (vec A M1))) (plus (cons_AV (vec A M1) (vec A C)) (cons_AV (vec A C) (vec A M')))). rewrite H6; rewrite H9; rewrite <- H8; auto. replace (plus (plus (cons_AV (vec A B) (vec A M)) (cons_AV (vec A B) (vec A M))) (plus (cons_AV (vec A M) (vec A C)) (cons_AV (vec A M) (vec A C)))) with (plus (plus (cons_AV (vec A B) (vec A M)) (cons_AV (vec A M) (vec A C))) (plus (cons_AV (vec A B) (vec A M)) (cons_AV (vec A M) (vec A C)))). replace (plus (cons_AV (vec A B) (vec A M)) (cons_AV (vec A M) (vec A C))) with (cons_AV (vec A B) (vec A C)). rewrite <- H1; rewrite add_mes_compatible; auto. rewrite Chasles; auto. mesure A B A M. mesure A M A C. replace (x + x0 + (x + x0)) with (x + x + (x0 + x0)); auto. ring. rewrite H6. rewrite Chasles; auto. generalize (non_axe_image_non_axe (A:=A) (B:=C) (M:=M) (M':=M')); intros. generalize (non_alignes_distincts (A:=A) (B:=C) (C:=M')); intros. rewrite Chasles; auto. rewrite Chasles; auto. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. elim existence_representant_unitaire with (A := A) (B := B); [ intros; try clear existence_representant_unitaire | auto ]. elim existence_representant_unitaire with (A := A) (B := M); [ intros; try clear existence_representant_unitaire | auto ]. elim alignes_representant_unitaire with (A := A) (B := B) (C := M); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. rewrite H11; auto. rewrite <- angles_representants_unitaires; auto. rewrite <- angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. replace (representant_unitaire (vec A B)) with (mult_PP (-1) (representant_unitaire (vec A M))). cut (A <> x0); intros. replace (mult_PP (-1) (representant_unitaire (vec A M))) with (vec x0 A). rewrite <- H10. rewrite <- angle_plat; auto. rewrite <- angle_plat; auto. rewrite <- H10. Ringvec. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := M) (C := x0); [ intros; elim H13; intros H22 H23; rewrite H22; try discrR | auto | auto ]. rewrite H11; Ringvec. rewrite H2. rewrite <- reflexion_axe; auto. generalize (non_axe_image_non_axe (A:=A) (B:=B) (M:=M) (M':=M1)); intros. generalize (non_alignes_distincts (A:=A) (B:=B) (C:=M1)); intros. elim (classic (alignes A C M1)); intros. cut (M' = M1); intros; auto. rewrite H9. generalize (axe_reflexion_bissectrice (A:=A) (B:=B) (M:=M) (M':=M1)); intros. apply rotation_def2; auto. generalize (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M1)); intros. elim H11; intros; auto. rewrite <- H9. cut (cons_AV (vec A M') (vec A C) = cons_AV (vec A C) (vec A M')); intros. replace (cons_AV (vec A M) (vec A M')) with (plus (plus (cons_AV (vec A M) (vec A B)) (cons_AV (vec A B) (vec A M1))) (plus (cons_AV (vec A M1) (vec A C)) (cons_AV (vec A C) (vec A M')))). rewrite <- H11; rewrite H10; auto. rewrite <- H9. replace (plus (plus (cons_AV (vec A B) (vec A M')) (cons_AV (vec A B) (vec A M'))) (plus (cons_AV (vec A M') (vec A C)) (cons_AV (vec A M') (vec A C)))) with (plus (plus (cons_AV (vec A B) (vec A M')) (cons_AV (vec A M') (vec A C))) (plus (cons_AV (vec A B) (vec A M')) (cons_AV (vec A M') (vec A C)))). replace (plus (cons_AV (vec A B) (vec A M')) (cons_AV (vec A M') (vec A C))) with (cons_AV (vec A B) (vec A C)). rewrite <- H1; rewrite add_mes_compatible; auto. rewrite H9; rewrite Chasles; auto. rewrite H9. mesure A B A M1. mesure A M1 A C. replace (x + x0 + (x + x0)) with (x + x + (x0 + x0)); auto. ring. rewrite H9; rewrite Chasles; auto. rewrite Chasles; auto. rewrite Chasles; auto. rewrite H9. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. elim existence_representant_unitaire with (A := A) (B := C); [ intros; try clear existence_representant_unitaire | auto ]. elim existence_representant_unitaire with (A := A) (B := M1); [ intros; try clear existence_representant_unitaire | auto ]. elim alignes_representant_unitaire with (A := A) (B := C) (C := M1); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. rewrite H13; auto. replace (representant_unitaire (vec A C)) with (mult_PP (-1) (representant_unitaire (vec A M1))). cut (A <> x0); intros. replace (mult_PP (-1) (representant_unitaire (vec A M1))) with (vec x0 A). rewrite <- H12. replace (mult_PP (-1) (vec A x0)) with (vec x0 A). rewrite <- angle_plat; auto. rewrite <- angle_plat; auto. Ringvec. rewrite <- H12. Ringvec. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := M1) (C := x0); [ intros; elim H15; intros H22 H23; rewrite H22; try discrR | auto | auto ]. rewrite H13; Ringvec. rewrite H3. rewrite <- reflexion_axe; auto. generalize (non_axe_image_non_axe (A:=A) (B:=C) (M:=M1) (M':=M')); intros. generalize (non_alignes_distincts (A:=A) (B:=C) (C:=M')); intros. generalize (axe_reflexion_bissectrice (A:=A) (B:=B) (M:=M) (M':=M1)); intros. generalize (axe_reflexion_bissectrice (A:=A) (B:=C) (M:=M1) (M':=M')); intros. apply rotation_def2; auto. generalize (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M1)); intros. generalize (reflexion_mediatrice (A:=A) (B:=C) (M:=M1) (M':=M')); intros. cut (distance A M = distance A M1); intros. rewrite H15. elim H13; intros; auto. elim H14; intros; auto. elim H13; intros; auto. replace (cons_AV (vec A M) (vec A M')) with (plus (plus (cons_AV (vec A M) (vec A B)) (cons_AV (vec A B) (vec A M1))) (plus (cons_AV (vec A M1) (vec A C)) (cons_AV (vec A C) (vec A M')))). rewrite <- H12; auto. rewrite H11; auto. replace (plus (plus (cons_AV (vec A B) (vec A M1)) (cons_AV (vec A B) (vec A M1))) (plus (cons_AV (vec A M1) (vec A C)) (cons_AV (vec A M1) (vec A C)))) with (plus (plus (cons_AV (vec A B) (vec A M1)) (cons_AV (vec A M1) (vec A C))) (plus (cons_AV (vec A B) (vec A M1)) (cons_AV (vec A M1) (vec A C)))). replace (plus (cons_AV (vec A B) (vec A M1)) (cons_AV (vec A M1) (vec A C))) with (cons_AV (vec A B) (vec A C)). rewrite <- H1; rewrite add_mes_compatible; auto. rewrite Chasles; auto. mesure A B A M1. mesure A M1 A C. replace (x + x0 + (x + x0)) with (x + x + (x0 + x0)); auto. ring. rewrite Chasles; auto. rewrite Chasles; auto. rewrite Chasles; auto. Qed.