proposition: Lemma g2_14 : forall A B C D, BetG A B A -> A <> B -> BetG C D C /\ BetG D C D.
proof: Proof. intros A B C D HBet1 HDiff1. split. { destruct (g2_11 A B D) as [E [HBet2 [HBet3 HDiff2]]]; auto. apply g2_13 with E; auto. } { destruct (g2_11 A B C) as [E [HBet2 [HBet3 HDiff2]]]; auto. apply g2_13 with E; auto. } Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le