proposition: Lemma axe_reflexion_droite : forall A B C M M' : PO, A <> B -> A <> C -> alignes A B C -> M' = reflexion A B M -> M' = reflexion C A M.
proof: Proof. intros A B C M M' H10 H0 H1 H2; try assumption. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H4; try clear existence_projete_orthogonal; try exact H3 | auto ]. halignes H1 k. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros | auto | auto ]. apply reflexion_def2 with H; auto. apply def_projete_orthogonal. auto. halignes H5 k0. elim (classic (k = 0)); intros. absurd (A = C); auto. rewrite H8 in H3. apply conversion_PP with (a := 1) (b := 1); auto with real. RingPP2 H3. Ringvec. apply colineaire_alignes with (/ k * (k + - k0)). replace (vec C H) with (add_PP (vec A H) (mult_PP (-1) (vec A C))). replace (vec C A) with (mult_PP (-1) (vec A C)). rewrite H7; rewrite H3. replace (mult_PP (/ k * (k + - k0)) (mult_PP (-1) (mult_PP k (vec A B)))) with (mult_PP (/ k * (k + - k0) * (-1 * k)) (vec A B)). replace (/ k * (k + - k0) * (-1 * k)) with (/ k * k * (-1 * (k + - k0))). replace (/ k * k) with 1. Ringvec. auto with real. ring. Ringvec. Ringvec. Ringvec. replace (vec C A) with (add_PP (mult_PP 0 (vec A B)) (mult_PP (- k) (vec A B))). apply ortho_combinaison_lineaire; auto. replace (vec C A) with (mult_PP (-1) (vec A C)). rewrite H3. Ringvec. Ringvec. rewrite (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); auto. Qed.