proposition: Lemma prop_27 : forall A D E F, TS E F A D -> CongA A E F D F E -> Par E A F D.
proof: Proof. intros A D E F. apply l12_21_b. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions