proposition: Lemma bet_lea__bet : forall A B C D E F, Bet A B C -> LeA A B C D E F -> Bet D E F.
proof: Proof. intros A B C D E F HBet Hlea. apply (bet_conga__bet A B C); auto. apply lea_asym; auto. apply lea_distincts in Hlea. spliter. apply l11_31_2; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2