proposition: Lemma paralleles_droites_plan : forall A B C D E : PO, ~ alignes A B C -> A <> B -> D <> E -> paralleles (droite A B) (droite D E) -> para_plan_dr (plan A B C) (droite D E).
proof: Proof. intros. apply def_para_plan_dr with (D := A) (E := B); auto with geo. Qed.