proposition: Lemma g2_11 : forall A B C, BetG A B A -> A <> B -> exists D, BetG C D C /\ BetG D C D /\ C <> D.
proof: Proof. intros A B C HBet1 HDiff1. destruct (segment_constructionG C C A B) as [D [HBet2 HCong1]]. assert (HDiff2 : C <> D) by (intro; apply g2_5 in HCong1; apply HDiff1; apply HCong1; auto). destruct (segment_constructionG C D B A) as [E [HBet3 HCong2]]. assert (HCong3 : CongG C E A A) by (apply g2_7 with D B; auto). assert (HEq : C = E) by (apply g2_5 in HCong3; apply HCong3; auto). rewrite HEq in *; clear HEq; exists D; do 2 (split; auto); apply g2_9; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le