proposition: Lemma bet_decG : forall A B C, BetG A B C \/ ~ BetG A B C.
proof: Proof. intros A B C. destruct (segment_constructionG A B B C) as [D [HBet1 HCong]]. elim (point_equality_decidabilityG C D); intro HDiff1; [rewrite HDiff1 in *; auto|]. elim (point_equality_decidabilityG A B); intro HDiff2; [rewrite HDiff2 in *; left; apply bet_symmetryG; apply between_trivialT|]. right; intro HBet2; apply HDiff1; apply construction_uniquenessT with A B B C; auto; apply g2_1. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le