proposition: Lemma l12_20 : forall A B C D, Par A B C D -> Cong A B C D -> TS A C B D -> Par B C D A /\ Cong B C D A /\ TS A C B D.
proof: Proof. intros. assert(TS B D A C). apply par_two_sides_two_sides. apply par_comm. assumption. assumption. assert(HH:=l12_20_bis A B C D H H0 H2). spliter. split. assumption. split. assumption. assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID