proposition: Lemma triangle_rectangle_une_fois : forall A B C : PO, triangle A B C -> orthogonal (vec A B) (vec A C) -> ~ orthogonal (vec A B) (vec B C) /\ ~ orthogonal (vec A C) (vec C B).
proof: Proof. intros. cut (triangle A C B); intros; auto with geo. deroule_triangle A C B. split; [ try assumption | idtac ]. red in |- *; intros; apply H2. elim orthogonal_paralleles with (A := A) (B := B) (C := C) (E := B) (F := C); [ intros k H7; try exact H7 | auto with geo | auto with geo | auto with geo | auto with geo ]. apply colineaire_alignes with (- k + 1); auto. replace (vec A B) with (add_PP (mult_PP (-1) (vec B C)) (vec A C)); [ idtac | Ringvec ]. rewrite H7; Ringvec. deroule_triangle A B C. red in |- *; intros; apply H6. elim orthogonal_paralleles with (A := A) (B := C) (C := B) (E := C) (F := B); [ intros k H11; try exact H11 | auto with geo | auto with geo | auto with geo | auto with geo ]. apply colineaire_alignes with (- k + 1); auto. replace (vec A C) with (add_PP (mult_PP (-1) (vec C B)) (vec A B)); [ idtac | Ringvec ]. rewrite H11; Ringvec. Qed.