proposition: Lemma orthogonales_2droites_secantes : forall A B C D E F G : PO, ~ alignes A B C -> D <> E -> F <> G -> coplanaires A B C F -> coplanaires A B C G -> orthogonales (droite A B) (droite D E) -> orthogonales (droite A C) (droite D E) -> orthogonales (droite F G) (droite D E).
proof: Proof. intros A B C D E F G H; try assumption. assert (A <> B); auto with geo. intros. apply def_orthogonales; auto. lapply (def_orthogonales2 (A:=A) (B:=B) (C:=D) (D:=E)); auto; intros. lapply (def_orthogonales2 (A:=A) (B:=C) (C:=D) (D:=E)); auto; intros. hcoplanaires H3 k k'. hcoplanaires H4 k0 k'0. replace (vec F G) with (add_PP (mult_PP (-1) (vec A F)) (vec A G)). rewrite H4. rewrite H3. replace (add_PP (mult_PP (-1) (add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)))) (add_PP (mult_PP k0 (vec A B)) (mult_PP k'0 (vec A C)))) with (add_PP (mult_PP (-1 * k + k0) (vec A B)) (mult_PP (-1 * k' + k'0) (vec A C))). Simplortho. Ringvec. Ringvec. apply non_alignes_distincts with B; auto. Qed.