proposition: Lemma l12_16 : forall A1 A2 B1 B2 C1 C2 X, Par A1 A2 B1 B2 -> Coplanar B1 B2 C1 C2 -> Inter A1 A2 C1 C2 X -> exists Y, Inter B1 B2 C1 C2 Y.
proof: Proof. intros. assert_diffs. apply cop_npar__inter; auto. destruct H1. auto. intro. apply inter__npar in H1. apply H1. apply par_trans with B1 B2; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID