proposition: Lemma coplanaires1_vecteur_def : forall A B C D : PO, coplanaires1 A B C D -> exists k : R, (exists k' : R, vec A D = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))).
proof: Proof. unfold coplanaires1, vec in |- *; intros. elim H; intros a H0; elim H0; intros b H1; try clear H0 H; try exact H1. exists b; auto. exists (1 + - (a + b)); auto. rewrite H1. RingPP. Qed.