proposition: Lemma similitude_conserve_orthogonalite : forall (I A B M A' B' M' : PO) (k a : R), k > 0 -> A' = similitude I k a A -> B' = similitude I k a B -> M' = similitude I k a M -> orthogonal (vec A B) (vec A M) -> orthogonal (vec A' B') (vec A' M').
proof: Proof. intros. assert (distance A' B' = k * distance A B). rewrite <- (distance_similitude (k:=k) (a:=a) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')) ; auto with geo. assert (distance A' M' = k * distance A M). rewrite <- (distance_similitude (k:=k) (a:=a) (I:=I) (A:=A) (B:=M) (A':=A') (B':=M')) ; auto with geo. discrimine A B. assert (distance A' B' = 0). rewrite H4; rewrite H6. replace (distance B B) with 0. ring. symmetry in |- *; 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. replace (distance M M) with 0. ring. symmetry in |- *; auto with geo. assert (A' = M'); auto with geo. rewrite H9. 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 similitude_conserve_angle with (a := a) (k := k) (I := I); auto. assert (double_AV (cons_AV (vec A B) (vec A M)) = image_angle pi). apply orthogonal_angles; auto with geo. assert (k <> 0); auto with real. apply angles_orthogonal. apply produit_distance_distinct with (3 := H4); auto. apply produit_distance_distinct with (3 := H5); auto. rewrite <- H8; auto. Qed.