proposition: Lemma par_trans : forall A1 A2 B1 B2 C1 C2, Par A1 A2 B1 B2 -> Par B1 B2 C1 C2 -> Par A1 A2 C1 C2.
proof: Proof. intros. apply playfair_implies_par_trans with B1 B2; [|assumption..]. unfold playfair_s_postulate. apply parallel_uniqueness. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID