proposition: Lemma g2_6 : forall A B, BetG A B B /\ CongG B B A A.
proof: Proof. intros A B; destruct (segment_constructionG A B A A) as [C [HBet HCong]]. assert (B = C) by (apply g2_5 with A A; auto). rewrite H in *; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le