proposition: Lemma g2_13 : forall A B C, BetG A B A -> A <> B -> BetG C B C.
proof: Proof. intros A B C HBet1 HDiff. destruct (segment_constructionG C B B C) as [D [HBet2 HCong1]]. assert (HEq : C = D) by (apply g2_8 with A B; try apply g2_2; try apply g2_12; auto). rewrite HEq in *; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le