proposition: Lemma g2_16 : forall A B C D E, ~ BetG C D E -> BetG A B A -> A = B.
proof: Proof. intros A B C D E HNBet HBet. elim (point_equality_decidabilityG A B); intro HDiff; auto. exfalso; apply HNBet; apply g2_15 with A B; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le