proposition: Lemma reflexion_conserve_orthogonalite : forall I J A A' B B' M M' : PO, I <> J -> A' = reflexion I J A :>PO -> B' = reflexion I J B :>PO -> M' = reflexion I J M :>PO -> orthogonal (vec A B) (vec A M) -> orthogonal (vec A' B') (vec A' M').
proof: Proof. intros. assert (distance A' B' = distance A B). rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=A) (M':=A') (N:=B) (N':=B')) ; auto with geo. assert (distance A' M' = distance A M). rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=A) (M':=A') (N:=M) (N':=M')) ; auto with geo. discrimine A B. assert (distance A' B' = 0). rewrite H4; rewrite H6; auto with geo. assert (A' = B'); auto with geo. rewrite H8. VReplace (vec B' B') zero; auto with geo. discrimine A M. assert (distance A' M' = 0). rewrite H5; rewrite H7; auto with geo. assert (A' = M'); auto with geo. rewrite H9. VReplace (vec M' M') zero; auto with geo. assert (~ alignes A B M); auto with geo. assert (B <> M); auto with geo. apply non_alignes_distincts2 with A; auto. assert (cons_AV (vec A' B') (vec A' M') = opp (cons_AV (vec A B) (vec A M))). apply reflexion_anti_deplacement with (A := I) (B := J); auto. assert (double_AV (cons_AV (vec A M) (vec A B)) = image_angle pi). apply orthogonal_angles; auto with geo. apply angles_orthogonal. apply (isometrie_distinct (A:=A) (B:=B) (A':=A') (B':=B')); auto. apply (isometrie_distinct (A:=A) (B:=M) (A':=A') (B':=M')); auto. rewrite H10. rewrite def_opp; auto. Qed.