proposition: Lemma le1234_lt__lt : forall A B C D E F, Le A B C D -> Lt C D E F -> Lt A B E F.
proof: Proof. intros A B C D E F Hle Hlt. destruct Hlt as [Hle' HNCong]. split. apply (le_transitivity _ _ C D); auto. intro. apply HNCong. apply le_anti_symmetry; auto. apply (l5_6 A B C D); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col