proposition: Lemma orthogonal_paralleles : forall A B C E F : PO, A <> B -> A <> C -> orthogonal (vec A B) (vec A C) -> orthogonal (vec E F) (vec A B) -> exists k : R, vec E F = mult_PP k (vec A C).
proof: Proof. intros. cut (repere_orthogonal A B C); intros. elim H3; intros. generalize (composantes_vecteur (O:=A) (I:=B) (J:=C) E F); intros. elim H6; [ intros x H7; elim H7; [ intros y H8; try clear H7 H6; try exact H8 ] | auto ]. cut (scalaire (vec E F) (vec A B) = 0); auto with geo; intros. cut (x = 0); intros. rewrite H8; rewrite H7. exists y. Ringvec. cut (x * scalaire (vec A B) (vec A B) = 0); intros. elim Rmult_integral with (r1 := scalaire (vec A B) (vec A B)) (r2 := x); [ intros H12; try clear without_div_Od; try trivial | intros H12; try trivial | try trivial ]. absurd (scalaire (vec A B) (vec A B) = 0); auto with geo. rewrite <- H7; ring. rewrite <- H6; auto with geo. rewrite H8. Simplscal. rewrite (scalaire_sym A C A B). rewrite H5; ring. apply triangle_rectangle_repere; auto with geo. Qed.