proposition: Lemma lt_right_comm : forall A B C D, Lt A B C D -> Lt A B D C.
proof: Proof. intros. unfold Lt in *. spliter. split. apply le_right_comm. assumption. intro. apply H0. apply cong_right_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col