proposition: Lemma points_plan_espace : forall A B C D E : PO, ~ coplanaires A B C D -> (exists k : R, (exists k' : R, vec D E = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)))) \/ (exists a : R, (exists b : R, (exists d : R, add_PP (cons d D) (cons (1 + - d) E) = add_PP (cons a A) (add_PP (cons b B) (cons (1 + - (a + b)) C))))).
proof: Proof. intros A B C D E H0; try assumption. assert (~ alignes A B C). elim non_coplanaires_expl with (A := A) (B := B) (C := C) (D := D); [ intros H H1; try clear non_coplanaires_expl; try exact H | try trivial ]. elim repere_espace with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros a H1; elim H1; intros b H2; elim H2; intros c H3; try clear H2 H1 repere_espace; try exact H3 | try trivial ]. elim (classic (a + b + c = 0)); intros. left. unfold vec in |- *. rewrite H3; rewrite H4. exists b; exists c. replace a with (- (b + c)). RingPP. replace a with (a + b + c + - (b + c)). rewrite H4; ring. ring. right. exists (/ (a + b + c) * a). exists (/ (a + b + c) * b). exists (/ (a + b + c) * (a + b + c + -1)). apply mult_PP_regulier with (a + b + c); auto. replace (mult_PP (a + b + c) (add_PP (cons (/ (a + b + c) * (a + b + c + -1)) D) (cons (1 + - (/ (a + b + c) * (a + b + c + -1))) E))) with (add_PP (cons (a + b + c + -1) D) (cons 1 E)). 2: FieldPP (a + b + c). rewrite H3. FieldPP (a + b + c). Qed.