proposition: Lemma cop4_par_perp2__par : forall A B C D E F G H, Par A B C D -> Perp A B E F -> Perp C D G H -> Coplanar A B E G -> Coplanar A B E H -> Coplanar A B F G -> Coplanar A B F H -> Par E F G H.
proof: Proof. apply par_perp_perp_implies_par_perp_2_par. intros A B; intros. apply (cop_par_perp__perp A B); assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID