proposition: Theorem axe_reflexion_bissectrice : forall A B M M' : PO, ~ alignes A B M -> M' = reflexion A B M -> cons_AV (vec A M) (vec A B) = cons_AV (vec A B) (vec A M').
proof: Proof. intros A B M M' H1 H2; try assumption. cut (A <> B); intros H0; [ idtac | auto with geo ]. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H4; try clear existence_projete_orthogonal; try exact H3 | auto ]. generalize (non_axe_image_non_axe (A:=A) (B:=B) (M:=M) (M':=M')); intros. generalize (non_alignes_distincts (A:=A) (B:=B) (C:=M')); intros. generalize (non_alignes_distincts (A:=A) (B:=B) (C:=M)); intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros; try exact H13 | auto | auto ]. elim (classic (A = H)); intros. generalize (reflexion_projete_orthogonal_milieu (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. apply milieu_angles_orthogonaux; auto. apply reflexion_image_distinct with (2 := H2); auto. rewrite H9; auto. generalize (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. replace (vec M M') with (add_PP (mult_PP (-1) (vec H M)) (mult_PP (-1) (vec H M))). apply ortho_combinaison_lineaire; apply ortho_sym; auto. rewrite H11; auto. Ringvec. cut (cons_AV (vec A M) (vec A H) = cons_AV (vec A H) (vec A M')); intros; auto. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. elim existence_representant_unitaire with (A := A) (B := H); [ intros; try clear existence_representant_unitaire | auto ]. elim existence_representant_unitaire with (A := A) (B := M'); [ 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 := H); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. rewrite H14. rewrite <- angles_representants_unitaires; auto. rewrite <- angles_representants_unitaires; auto. replace (representant_unitaire (vec A B)) with (mult_PP (-1) (representant_unitaire (vec A H))). cut (A <> x); intros. replace (mult_PP (-1) (representant_unitaire (vec A H))) with (vec x A). replace (cons_AV (representant_unitaire (vec A M)) (vec x A)) with (plus (cons_AV (representant_unitaire (vec A M)) (vec A x)) (cons_AV (vec A x) (vec x A))). replace (cons_AV (vec x A) (representant_unitaire (vec A M'))) with (plus (cons_AV (vec x A) (vec A x)) (cons_AV (vec A x) (representant_unitaire (vec A M')))). rewrite <- angle_plat; auto. rewrite <- angle_plat; auto. rewrite H11. rewrite <- angles_representants_unitaires; auto. rewrite <- angles_representants_unitaires; auto. rewrite <- H10; auto. mesure A M A H. replace (x2 + pi) with (pi + x2); (try ring; auto). rewrite <- H12. cut (A <> x0); intros. rewrite Chasles; auto. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := M') (C := x0); [ intros; elim H17; intros H22 H23; try clear H17 def_representant_unitaire2; rewrite H22; try discrR | auto | auto ]. rewrite <- H13. cut (A <> x1); intros. rewrite Chasles; auto. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := M) (C := x1); [ intros; elim H17; intros H22 H23; try clear H18 def_representant_unitaire2; rewrite H22; try discrR | auto | auto ]. rewrite <- H11; Ringvec. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := H) (C := x); [ intros; elim H16; intros H22 H23; try clear H18 def_representant_unitaire2; rewrite H22; try discrR | auto | auto ]. rewrite H14. elim existence_representant_unitaire with (A := A) (B := B); [ intros; try clear existence_representant_unitaire | auto ]. rewrite <- H15; Ringvec. generalize (reflexion_image_distinct (A:=A) (B:=B) (M:=M) (M':=M')); intros. generalize (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M')); intros. elim H11; auto; intros. generalize (reflexion_projete_orthogonal_milieu (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. apply mediatrice_milieu_angles; auto. Qed.