proposition: Lemma prop_5_2 : forall A B C F G, A <> B -> B <> C -> Cong A B A C -> Bet A B F -> B <> F -> Bet A C G -> C <> G -> CongA F B C G C B.
proof: Proof. intros A B C F G. intros. apply l11_13 with A A; auto. apply l11_44_1_a; auto. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions