proposition: Lemma projete_absolu_cos : forall (A B C H : PO) (a : R), A <> B -> A <> C -> H = projete_orthogonal A B C -> image_angle a = cons_AV (vec A B) (vec A C) -> distance A H = distance A C * Rabs (cos a).
proof: Proof. intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H); [ intros; auto | auto | auto ]. halignes H4 k. cut (orthogonal (vec H A) (vec H C)); intros; auto with geo. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H8; try clear total_order | intros H8; elim H8; [ intros H9; try clear H8 | intros H9; try clear H8; try exact H9 ] ]. replace (Rabs (cos a)) with (Rabs (cos (a + pi))). apply triangle_rectangle_absolu_cos; auto. apply distinct_produit_vecteur with (3 := H6); auto with real. rewrite H6; auto. rewrite angle_produit_negatif_l; auto. rewrite add_mes_compatible; rewrite <- H3; auto. RReplace (a + pi) (pi + a). elim pi_plus_x with (x := a); [ intros H9 H10; try clear pi_plus_x; rewrite H9 ]. rewrite Rabs_Ropp; auto. cut (A = H); intros. rewrite <- H8 in H5; auto. elim droit_direct_ou_indirect with (A := A) (B := B) (C := C); [ intros H10; try clear droit_direct_ou_indirect | intros H10; try clear droit_direct_ou_indirect; try exact H10 | auto | auto | auto ]. replace (cos a) with (cos pisurdeux). rewrite cos_pisurdeux; rewrite Rabs_R0; ring_simplify. rewrite <- H8; auto with geo. apply cos_deux_mes. rewrite H10; auto. replace (cos a) with (cos (- pisurdeux)). rewrite cos_paire; rewrite cos_pisurdeux; rewrite Rabs_R0; ring_simplify. rewrite <- H8; auto with geo. apply cos_deux_mes. rewrite H10; auto. apply produit_zero_conf with (1 := H6); auto. apply triangle_rectangle_absolu_cos; auto. apply distinct_produit_vecteur with (3 := H6); auto with real. rewrite H6; auto. rewrite angle_produit_positif_l; auto. replace (vec H A) with (mult_PP (- k) (vec A B)). Simplortho. VReplace (vec H A) (mult_PP (-1) (vec A H)). rewrite H6; Ringvec. Qed.