proposition: Lemma existence_coordonnees : forall O I J M : PO, repere O I J -> exists x : R, (exists y : R, vec O M = 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'. exists k; exists k'; auto. Qed.