proposition: Lemma composantes_vecteur : forall O I J M N : PO, repere O I J -> exists x : R, (exists y : R, vec M N = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J))).
proof: Proof. unfold repere, triangle in |- *; intros. assert (coplanaires O I J M); auto with geo. hcoplanaires H0 k k'. assert (coplanaires O I J N); auto with geo. hcoplanaires H1 k0 k'0. replace (vec M N) with (add_PP (vec O N) (mult_PP (-1) (vec O M))). rewrite H1; rewrite H0. exists (k0 + -1 * k); exists (k'0 + -1 * k'). Ringvec. Ringvec. Qed.