proposition: Lemma lt_left_comm : forall A B C D, Lt A B C D -> Lt B A C D.
proof: Proof. intros. unfold Lt in *. spliter. split. unfold Le in *. ex_and H P. exists P. apply cong_left_commutativity in H1. split; assumption. intro. apply H0. apply cong_left_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col