proposition: Lemma tetraedre_non_alignes : forall A B C D : PO, tetraedre A B C D -> ~ alignes A B C.
proof: Proof. unfold tetraedre in |- *; intros. elim non_coplanaires_expl with (A := A) (B := B) (C := C) (D := D); [ intros H0 H1; try clear non_coplanaires_expl; try exact H0 | auto ]. Qed.