proposition: Lemma bet__lt1213 : forall A B C, B <> C -> Bet A B C -> Lt A B A C.
proof: Proof. intros A B C HBC HBet. split. apply bet__le1213; trivial. intro. apply HBC, between_cong with A; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col