proposition: Lemma segment_construction_B : forall A B C D, A<>B -> exists E, T A B E /\ Cong B E C D.
proof: Proof. intros A B C D HDiff. assert (T := segment_construction A B C D). destruct T as [E [HBet HCong]]. apply Bet_T in HBet. exists E; intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality