proposition: Lemma lt_diff : forall A B C D, Lt A B C D -> C <> D.
proof: Proof. intros A B C D HLt Heq. subst D. destruct HLt as [HLe HNCong]. assert (A = B) by (apply le_zero with C; assumption). subst B; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col