proposition: Lemma l2_11T : forall A B C A' B' C', BetG A B C -> BetG A' B' C' -> CongG A B A' B' -> CongG B C B' C' -> CongG A C A' C'.
proof: Proof. intros A B C A' B' C' HBet1 HBet2 HCong1 HCong2. elim (point_equality_decidabilityG A B); intro HDiff; [rewrite HDiff in *; clear HDiff|]. { assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto). rewrite HEq in *; auto. } { apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto; try apply cong_trivial_identityT; 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