proposition: Lemma g2_8 : forall A B C D, BetG A B C -> BetG A B D -> CongG B C B D -> A <> B -> C = D.
proof: Proof. intros A B C D HBet1 HBet2 HCong HDiff. assert (HEq : CongG C C C D). { apply five_segmentG with A A B B; auto; try apply g2_1. apply g2_7 with B B; auto; apply g2_1. } apply g2_5 with C C; auto; apply g2_2; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le