proposition: Lemma prop_7 : forall A B C C', Cong A C A C' -> Cong B C B C' -> OS A B C C' -> C = C'.
proof: Proof. intros A B C C' HCongA HCongB HOS. assert (HNCol := one_side_not_col123 A B C C' HOS). assert_diffs. destruct (l11_51 A B C A B C') as [HCongAA [HCongAB HCongAC]]; Cong. apply (l6_21 A C B C); Col; apply out_col. apply (conga_os__out B); Side. apply (conga_os__out A); assumption. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions