proposition: Lemma vecteurs_para_plan_dr : forall (A B C D E : PO) (k k' : R), D <> E -> ~ alignes A B C -> vec D E = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)) -> para_plan_dr (plan A B C) (droite D E).
proof: Proof. intros. cut (ex (fun F : PO => vec A F = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)))); intros. elim H2; intros F H3; try clear H2; try exact H3. cut (vec A F = vec D E); intros. cut (A <> F). intros H30. apply def_para_plan_dr with (D := A) (E := F); auto with geo. unfold vec in H2. apply vecteur_def_coplanaires with (1 := H3); auto with geo. apply colineaires_paralleles with 1; auto with geo. rewrite H2; Ringvec. unfold not in |- *; intros; apply H. apply conversion_PP with (a := 1) (b := 1); auto with *. cut (vec D E = vec A F); intros. RingPP2 H5. rewrite H4. unfold vec in |- *. RingPP. auto with *. rewrite H3; auto. elim (classic (k' = - k)); intros. rewrite H2. replace (add_PP (mult_PP k (vec A B)) (mult_PP (- k) (vec A C))) with (mult_PP k (vec C B)). elim existence_representant_mult_vecteur with (A := A) (B := C) (C := B) (k := k); intros D0 H3; try clear existence_representant_mult_vecteur; try exact H3. exists D0; auto. unfold vec in |- *; RingPP. exists (barycentre (cons (1 + - (k + k')) A) (cons (k + k') (barycentre (cons k B) (cons k' C)))). unfold vec in |- *. replace 1 with (1 + - (k + k') + (k + k')) at 1 by ring. rewrite <- add_PP_barycentre; try lra. rewrite <- add_PP_barycentre; try lra. RingPP. Qed.