proposition: Lemma l12_21 : forall A B C D, TS A C B D -> (CongA B A C D C A <-> Par A B C D).
proof: Proof. intros. split. intro. apply l12_21_b ; assumption. intro. apply l12_21_a; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID