proposition: Lemma l12_21_a : forall A B C D, TS A C B D -> (Par A B C D -> CongA B A C D C A).
proof: Proof. apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right). Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID