proposition: Lemma g2_7 : forall A B C A' B' C', CongG A B A' B' -> CongG B C B' C' -> BetG A B C -> BetG A' B' C' -> CongG A C A' C'.
proof: Proof. intros A B C A' B' C' HCong1 HCong2 HBet1 HBet2. elim (point_equality_decidabilityG A B); intro HDiff1; [rewrite HDiff1 in *; clear HDiff1|]. { assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto). rewrite HEq; auto. } { elim (g2_6 A' A); intro HBet3; intro HCong3. apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto. apply g2_3; apply g2_4; auto. } Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le