proposition: Lemma prop_6 : forall A B C, ~ Col A B C -> CongA A B C A C B -> Cong A B A C.
proof: Proof. intros A B C H. apply l11_44_1_b; Col. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions