proposition: Lemma out_lea__out : forall A B C D E F, Out E D F -> LeA A B C D E F -> Out B A C.
proof: Proof. intros A B C D E F Hout Hlea. apply (l11_21_a D E F); auto. apply lea_asym; auto. apply lea_distincts in Hlea. spliter. apply l11_31_1; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2