proposition: Lemma l11_62_unicity_bis : forall A B C U X Y, Orth_at X A B C X U -> Orth_at Y A B C Y U -> X = Y.
proof: Proof. unfold Orth_at. intros A B C U X Y HX HY. spliter. apply l11_62_unicity with A B C U; trivial; intros; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2