proposition: Lemma ColB_Col : forall A B C, ColB A B C -> Col A B C.
proof: Proof. intros A B C HCol. unfold ColB in HCol. unfold Col. elim (T_dec A B C); intro HT1; elim (T_dec A C B); intro HT2; elim (T_dec C A B); intro HT3. apply T_Bet in HT1; intuition. apply T_Bet in HT1; intuition. apply T_Bet in HT1; intuition. apply T_Bet in HT1; intuition. apply T_Bet in HT2; intuition. apply T_Bet in HT2; intuition. apply T_Bet in HT3; intuition. exfalso; apply HCol; intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality