proposition: Lemma bet_cop2__cop : forall A B C U V W, Coplanar A B C U -> Coplanar A B C W -> Bet U V W -> Coplanar A B C V.
proof: Proof. intros A B C U V W HU HW HBet. destruct (eq_dec_points U W). treat_equalities; assumption. apply col_cop2__cop with U W; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar