proposition: Lemma vecteur_def_coplanaires : 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)) -> coplanaires A B C D.
proof: Proof. intros; unfold coplanaires in |- *. right; try assumption. apply vecteur_def_coplanaires1 with (k := k) (k' := k'); try assumption. Qed.