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