proposition: Lemma lemma_togethera : forall A B C D F G P Q a b c : Point, TG A a B b C c -> Cong D F A a -> Cong F G B b -> BetS D F G -> Cong P Q C c -> Lt P Q D G.
proof: Proof. intros. apply (lemma_together A B C D F G P Q a b c);auto. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_lessthannotequal GeoCoq.Elements.OriginalProofs.lemma_together GeoCoq.Elements.OriginalProofs.lemma_ray5 GeoCoq.Elements.OriginalProofs.lemma_subtractequals GeoCoq.Elements.OriginalProofs.lemma_ondiameter