proposition: Lemma par_strict_cong_mid : forall A B A' B', Par_strict A B A' B' -> Cong A B A' B' -> exists M, Midpoint M A A' /\ Midpoint M B B' \/ Midpoint M A B' /\ Midpoint M B A'.
proof: Proof. intros A B A' B' HParS HCong. assert (HP:=parallel_uniqueness). destruct (midpoint_existence A A') as [M1 HM1]. destruct (symmetric_point_construction B M1) as [B'' HB'']. assert (HCol1 : Col B'' A' B'). { assert (Col A' A' B' /\ Col B'' A' B'); [|spliter; Col]. assert (HPar := par_strict_par A B A' B' HParS). apply HP with A B A'; Col. assert_diffs; apply l12_17 with M1; Col. } assert (HCong1 : Cong A' B' A' B'') by (assert (H := l7_13 M1 A' B'' A B HM1 HB''); eCong). destruct (midpoint_existence A B') as [M2 HM2]. destruct (symmetric_point_construction B M2) as [A'' HA'']. assert (HCol2 : Col A'' A' B'). { assert (Col B' A' B' /\ Col A'' A' B'); [|spliter; Col]. assert (HPar := par_strict_par A B A' B' HParS). apply HP with A B B'; Col. assert_diffs; apply l12_17 with M2; Col. } assert (HCong2 : Cong A' B' B' A'') by (assert (H := l7_13 M2 B' A'' A B HM2 HA''); eCong). elim (l7_20 A' B' B''); Col; intro HElim1; treat_equalities. { exists M1; left; Col. } { elim (l7_20 B' A' A''); Cong; Col; intro HElim2; treat_equalities. { exists M2; right; Col. } { exfalso; destruct (outer_pasch B' A A' B'' M1) as [I [HAIB' HA''IM1]]; unfold Midpoint in*; spliter; Between. assert (HM1I : M1 <> I). { intro; treat_equalities. assert_cols; show_distinct A M1; apply HParS; exists A; split; ColR. } assert (HB''M1 : B'' <> M1). { intro; treat_equalities; apply HParS; exists B; Col. } elim (l5_2 B'' M1 I B); Between; intro HBM1I. { show_distinct B' A''; [apply HParS; exists A; split; Col|]. show_distinct A' B'; [apply HParS; exists A; split; Col|]. assert (HFalse : TS A B' B A''). { split; [intro; apply HParS; exists B'; split; Col|]. split; [assert_cols; intro; apply HParS; exists A; split; ColR|]. exists M2; split; Col. } apply (l9_9 A B' B A''); trivial. exists A'; split. { show_distinct B' B''; [apply HParS; exists A; split; Col|]. assert (~ Col B'' A B') by (intro; apply HParS; exists A; split; ColR). apply l9_2; apply l9_8_2 with B''. { destruct HFalse. repeat split; Col. exists I; split; [Col|eBetween]. } { apply l9_19 with B'; Col. repeat split; Col. } } { split; [destruct HFalse as [_ []]; Col|]. split; [intro; apply HParS; exists A; split; Col|]. exists B'; split; Col; Between. } } { show_distinct A' B'; [apply HParS; exists A; split; Col|]. show_distinct A' B''; [apply HParS; exists A; split; Col|]. assert (HFalse : OS A A' B B'). { exists B''; split. { split; [intro; apply HParS; exists A'; split; Col|]. split; [intro; apply HParS; exists A; split; ColR|]. exists M1; split; Col. } { apply invert_two_sides, bet__ts; auto. intro; apply HParS; exists A; split; Col. } } apply l9_9_bis in HFalse; apply HFalse; clear HFalse; apply l9_31. { apply l12_6, HParS. } { apply one_side_transitivity with B''. { apply l9_19 with B'; Col. split; [|intro; apply HParS; exists A; split; Col]. repeat split; [intro; treat_equalities; apply HParS; exists A; split; Col..|Between]. } { apply out_one_side_1 with I; Col; [intro; apply HParS; exists A; split; ColR|]. split; [intro; treat_equalities; auto|]. split; [intro; treat_equalities; apply HParS; exists B'; split; Col|]. right; eBetween. } } } } } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates