proposition: Lemma l12_22_a : forall A B C D P, Out P A C -> OS P A B D -> Par A B C D -> CongA B A P D C P.
proof: Proof. cut (forall A B C D P, A <> P -> Bet P A C -> OS P A B D -> Par A B C D -> CongA B A P D C P). { intros Haux A B C D P HOut HOS HPar. destruct HOut as [HAP [HCP [|]]]. apply Haux; trivial. apply conga_sym, Haux; Par. apply col_one_side with A; Col; Side. } intros A B C D P HAP HBet HOS HPar. destruct (eq_dec_points A C). { subst C. apply out2__conga; [|apply out_trivial; auto]. apply col_one_side_out with P; Side. apply par_id; Par. } destruct (segment_construction B A B A) as [B' []]. assert_diffs. apply conga_trans with B' A C. apply l11_14; auto. apply l11_10 with B' C D A; try (apply out_trivial); auto; [|apply l6_6, bet_out; Between]. apply l12_21_a; [|apply par_col_par_2 with B; Col]. apply l9_2, l9_8_2 with B; [|apply col_one_side with P; Side; Col]. assert (HNCol : ~ Col P A B) by (apply one_side_not_col123 with D, HOS). assert (HNCol1 : ~ Col B A C) by (intro; apply HNCol; ColR). repeat split; trivial. intro; apply HNCol1; ColR. exists A; Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID