proposition: Lemma g2_15 : forall A B C D E, BetG A B A -> A <> B -> BetG C D E.
proof: Proof. intros A B C D E HBet HDiff. apply g2_9. destruct (g2_14 A B D E) as [HBet1 HBet2]; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le