proposition: Lemma para_plan_dr_vecteur : forall A B C D E : PO, D <> E :>PO -> ~ alignes A B C -> para_plan_dr (plan A B C) (droite D E) -> exists k : R, (exists k' : R, vec D E = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))).
proof: Proof. intros A B C D E H30 H H0; unfold vec in |- *. elim def_para_plan_dr2 with (A := A) (B := B) (C := C) (F := D) (G := E); [ intros F H2; elim H2; intros G H3; try clear H2; try exact H3 | auto | auto | auto ]. elim H3; intros H2 H4; elim H4; intros H5 H6; try clear H4 H3; try exact H6. elim H2; [ intros H1 H3; try clear H2; try exact H3 ]. hPPcoplanaires H1 a0 b0. hPPcoplanaires H3 a1 b1. generalize (def_paralleles2 (A:=D) (B:=E) (C:=F) (D:=G)); intros H9. elim H9; [ intros k H2; try clear H9; try exact H1 | auto with geo | auto with geo | auto with geo ]. replace (add_PP (cons (-1) D) (cons 1 E)) with (add_PP (cons 1 E) (cons (-1) D)). rewrite H2. replace (cons k G) with (mult_PP k (cons 1 G)). replace (cons (- k) F) with (mult_PP (- k) (cons 1 F)). rewrite H3. rewrite H1. exists (k * (b1 + - b0)); exists (k * (a0 + b0 + - (a1 + b1))). RingPP. RingPP. RingPP. RingPP. Qed.