proposition: Lemma g2_9 : forall A B C, BetG A B A -> BetG C A B.
proof: Proof. intros A B C HBet. apply bet_inner_transitivityG with A; auto; apply g2_6. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le