proposition: Lemma rotation_conserve_orthogonalite : forall (I A B M A' B' M' : PO) (a : R), A' = rotation I a A -> B' = rotation I a B -> M' = rotation I a M -> 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 <- (rotation_isometrie (I:=I) (A:=A) (B:=B) (A':=A') (B':=B') (a:=a)); auto with geo. assert (distance A' M' = distance A M). rewrite <- (rotation_isometrie (I:=I) (A:=A) (B:=M) (A':=A') (B':=M') (a:=a)); auto with geo. discrimine A B. assert (distance A' B' = 0). rewrite H3; rewrite H5; auto with geo. assert (A' = B'); auto with geo. rewrite H7. VReplace (vec B' B') zero; auto with geo. discrimine A M. assert (distance A' M' = 0). rewrite H4; rewrite H6; auto with geo. assert (A' = M'); auto with geo. rewrite H8. VReplace (vec M' M') zero; auto with geo. assert (cons_AV (vec A B) (vec A M) = cons_AV (vec A' B') (vec A' M')). apply rotation_conserve_angle with (a := a) (I := I); auto. assert (double_AV (cons_AV (vec A B) (vec A M)) = 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 <- H7; auto. Qed.