proposition: Lemma couple_vecteurs_coplanaires : forall (A B C D E F : PO) (a b c d : R), ~ alignes A B C -> ~ alignes D E F -> vec D E = add_PP (mult_PP a (vec A B)) (mult_PP b (vec A C)) :>PP -> vec D F = add_PP (mult_PP c (vec A B)) (mult_PP d (vec A C)) :>PP -> para_plan_plan (plan A B C) (plan D E F).
proof: Proof. intros. deroule_triangle D E F. apply def_para_plan_plan; auto. apply vecteurs_para_plan_dr with (k := a) (k' := b); auto. apply vecteurs_para_plan_dr with (k := c) (k' := d); auto. Qed.