proposition: Lemma paralleles_droite_plan_coplanaires_incluse : forall A B C D E : PO, D <> E :>PO -> ~ alignes A B C -> para_plan_dr (plan A B C) (droite D E) -> coplanaires A B C D -> coplanaires A B C E.
proof: Proof. intros A B C D E H20 H H0 H1. unfold coplanaires in |- *. hPPcoplanaires H1 a1 b1. elim def_para_plan_dr2 with (3 := H0); auto. intros F H2; elim H2; intros G H3; elim H3; intros H4 H5; elim H5; intros H6 H7; try clear H5 H3 H2; try exact H7. elim H4; [ intros H2 H3; try clear H4; try exact H3 ]. hPPcoplanaires H2 a b. hPPcoplanaires H3 a0 b0. cut (paralleles (droite D E) (droite F G)); intros; auto with geo. elim def_paralleles2 with (3 := H4); auto; intros. right; try assumption. exists (x * a0 + (- x * a + a1)). exists (x * b0 + (- x * b + b1)). RingPP1 H5. VReplace (cons x G) (mult_PP x (cons 1 G)). VReplace (cons (- x) F) (mult_PP (- x) (cons 1 F)). VReplace (mult_PP (-1) (cons (-1) D)) (cons 1 D). rewrite H1; rewrite H3; rewrite H2. RingPP. Qed.