proposition: Lemma projete_negatif_cos : forall (A B C H : PO) (a k : R), A <> B -> A <> C -> H = projete_orthogonal A B C -> vec A H = mult_PP k (vec A B) -> k < 0 -> image_angle a = cons_AV (vec A B) (vec A C) -> cos a < 0.
proof: Proof. intros. cut (scalaire (vec A B) (vec A C) < 0); intros. replace (cos a) with (/ distance A B * / distance A C * scalaire (vec A B) (vec A C)). RReplace 0 (/ distance A B * / distance A C * 0). apply Rmult_lt_compat_l; auto with real. apply Rmult_lt_0_compat; auto with real. apply Rinv_0_lt_compat; auto with real. cut (distance A B >= 0); intros; auto with geo. elim H7; auto with real; intros. absurd (distance A B = 0); auto with geo. apply Rinv_0_lt_compat; auto with real. cut (distance A C >= 0); intros; auto with geo. elim H7; auto with real; intros. absurd (distance A C = 0); auto with geo. rewrite (produit_scalaire_cosinus (A:=A) (B:=B) (C:=C) (a:=a)); auto. field; split; auto with geo. elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H); [ intros; auto | auto | auto ]. rewrite (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=H)); auto with geo. rewrite H3. RReplace (scalaire (vec A B) (mult_PP k (vec A B))) (- (- k * scalaire (vec A B) (vec A B))). apply Ropp_lt_gt_0_contravar; auto with real. apply Rmult_gt_0_compat; auto with real. cut (scalaire (vec A B) (vec A B) >= 0); intros; auto with geo. elim H8; auto with real; intros. absurd (scalaire (vec A B) (vec A B) = 0); auto with geo. Simplscal. Qed.