proposition: Lemma lea456789_lta__lta : forall A B C D E F G H I, LtA A B C D E F -> LeA D E F G H I -> LtA A B C G H I.
proof: Proof. intros A B C D E F G H I Hlta Hlea. split. - apply (lea_trans _ _ _ D E F). apply lta__lea; assumption. assumption. - intro. destruct Hlta as [Hlea' HNConga]. apply HNConga. apply lea_asym. assumption. apply (l11_30 D E F G H I); auto; [|apply conga_sym; assumption]. apply lea_distincts in Hlea. spliter. apply conga_refl; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2