proposition: Lemma para_plan_refl : forall A B C : PO, ~ alignes A B C -> para_plan_plan (plan A B C) (plan A B C).
proof: Proof. intros. deroule_triangle A B C. generalize (couple_vecteurs_coplanaires (A:=A) (B:=B) (C:=C) (D:=A) (E:=B) (F:=C) (a:=1) (b:=0) (c:=0) (d:=1)); intros H11; apply H11; auto. unfold vec in |- *; RingPP. unfold vec in |- *; RingPP. Qed.