proposition: Lemma vecteur_def_coplanaires1 : forall (k k' : R) (A B C D : PO), vec A D = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)) -> coplanaires1 A B C D.
proof: Proof. unfold coplanaires1, vec in |- *; intros. exists (1 + - (k + k')); auto. exists k; auto. RingPP2 H. RingPP. Qed.