proposition: Lemma projete_distance_Rlt : forall A B C H : PO, A <> B -> H <> B -> H = projete_orthogonal A B C -> distance C H < distance C B.
proof: Proof. intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H); [ intros | auto | auto ]. elim (Pythagore H B C); intros. assert (Rsqr (distance C H) < Rsqr (distance C B)). rewrite (distance_sym C B). rewrite H5; auto. RReplace (Rsqr (distance C H)) (Rsqr (distance C H) + 0). assert (0 < Rsqr (distance H B)). assert (distance H B <> 0); auto with geo. cut (0 <= distance H B); auto with geo real. RReplace (Rsqr (distance H B) + Rsqr (distance H C)) (Rsqr (distance H C) + Rsqr (distance H B)). rewrite distance_sym; auto with real. halignes H3 k. VReplace (vec H B) (add_PP (vec A B) (mult_PP (-1) (vec A H))). rewrite H7. VReplace (add_PP (vec A B) (mult_PP (-1) (mult_PP k (vec A B)))) (mult_PP (1 + - k) (vec A B)). auto with geo. apply Rsqr_incrst_0; auto with real geo. Qed.