proposition: Lemma lt_transitivity : forall A B C D E F, Lt A B C D -> Lt C D E F -> Lt A B E F.
proof: Proof. intros A B C D E F HLt1 HLt2. apply le1234_lt__lt with C D; try (apply lt__le); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col