proposition: Lemma prop_33 : forall A B C D, TS B C A D -> Par A B C D -> Cong A B C D -> Cong A C B D /\ Par A C B D.
proof: Proof. intros A B C D HTS HPAR HC. assert (HPara:Parallelogram B A C D) by (left;split;finish). destruct (plg_cong B A C D HPara). assert_diffs. destruct (plg_par B A C D); auto. split; [Cong|Par]. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions