proposition: Lemma cong2_lt__lt : forall A B C D A' B' C' D', Lt A B C D -> Cong A B A' B' -> Cong C D C' D' -> Lt A' B' C' D'.
proof: Proof. intros A B C D A' B' C' D' Hlt HCong1 HCong2. destruct Hlt as [Hle HNCong]. split. apply (l5_6 A B C D); auto. intro. apply HNCong. apply (cong_transitivity _ _ A' B'); auto. apply (cong_transitivity _ _ C' D'); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col