proposition: Lemma cop_per2__col : forall A X Y Z, Coplanar A X Y Z -> A <> Z -> Per X Z A -> Per Y Z A -> Col X Y Z.
proof: Proof. intros A X Y Z HC HAZ HPer1 HPer2. destruct HPer1 as [B' [HMid1 HCong1]]; destruct HPer2 as [B [HMid2 HCong2]]; treat_equalities. elim (eq_dec_points X Y); intro HXY; treat_equalities; Col. elim (eq_dec_points X Z); intro HXZ; treat_equalities; Col. elim (eq_dec_points Y Z); intro HYZ; treat_equalities; Col. destruct HC as [I HC]. elim HC; clear HC; intro HC; try (elim HC; clear HC); try (intros HCol1 HCol2); try (intro H; destruct H as [HCol1 HCol2]). { elim (eq_dec_points X I); intro HXI; treat_equalities; Col. assert (HCong3 : Cong I A I B) by (apply l4_17 with Y Z; unfold Midpoint in *; spliter; Cong). elim HCol1; clear HCol1; intro HCol1; try (elim HCol1; clear HCol1; intro HCol1). { assert (HLe : Le A X B I). { apply l5_6 with A X A I; Cong. apply l6_13_2; Col. split; try (intro; treat_equalities; Col). split; try (intro; treat_equalities; Col); Col. } assert (H := le_bet B I A X HLe); destruct H as [X' [HBet HCong4]]; clear HLe. assert (HCong5 : Cong A X' B X). { apply five_segment with I I X X'; Cong; Between. apply l4_3 with A B; Cong; Between. apply l4_3 with B A; Cong; Between. } assert (H : X = X'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col. apply cong_transitivity with B X; Cong. apply l4_3 with A B; Cong; Between. } assert (H : A = B) by (apply construction_uniqueness with I X X A; Cong; Between); treat_equalities; intuition. } { assert (H := segment_construction B I I X); destruct H as [X' [HBet HCong4]]. assert (HCong5 : Cong A X' B X). { apply five_segment with X X' I I; Cong; Between. } assert (H : X = X'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col; Cong. apply cong_transitivity with B X; Cong. } assert (H : A = B) by (apply construction_uniqueness with X I I A; Cong; Between); treat_equalities; intuition. } { assert (H := segment_construction I B A X); destruct H as [X' [HBet HCong4]]. assert (HCong5 : Cong X B X' A). { apply five_segment with I I A B; Cong; intro; treat_equalities; Col. } assert (H : X = X'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col. apply cong_transitivity with B X; Cong. apply l2_11 with A B; Cong. } assert (H : A = B) by (apply between_cong_2 with I X; Col). treat_equalities; intuition. } } { elim (eq_dec_points Y I); intro HYI; treat_equalities; Col. assert (HCong3 : Cong I A I B) by (apply l4_17 with X Z; unfold Midpoint in *; spliter; Cong). elim HCol1; clear HCol1; intro HCol1; try (elim HCol1; clear HCol1; intro HCol1). { assert (HLe : Le A Y B I). { apply l5_6 with A Y A I; Cong. apply l6_13_2; Col. split; try (intro; treat_equalities; Col). split; try (intro; treat_equalities; Col); Col. } assert (H := le_bet B I A Y HLe); destruct H as [Y' [HBet HCong4]]; clear HLe. assert (HCong5 : Cong A Y' B Y). { apply five_segment with I I Y Y'; Cong; Between. apply l4_3 with A B; Cong; Between. apply l4_3 with B A; Cong; Between. } assert (H : Y = Y'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col. apply cong_transitivity with B Y; Cong. apply l4_3 with A B; Cong; Between. } assert (H : A = B) by (apply construction_uniqueness with I Y Y A; Cong; Between); treat_equalities; intuition. } { assert (H := segment_construction B I I Y); destruct H as [Y' [HBet HCong4]]. assert (HCong5 : Cong A Y' B Y). { apply five_segment with Y Y' I I; Cong; Between. } assert (H : Y = Y'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col; Cong. apply cong_transitivity with B Y; Cong. } assert (H : A = B) by (apply construction_uniqueness with Y I I A; Cong; Between); treat_equalities; intuition. } { assert (H := segment_construction I B A Y); destruct H as [Y' [HBet HCong4]]. assert (HCong5 : Cong Y B Y' A). { apply five_segment with I I A B; Cong; intro; treat_equalities; Col. } assert (H : Y = Y'); treat_equalities. { apply l4_18 with A I; try (intro; treat_equalities); Col. apply cong_transitivity with B Y; Cong. apply l2_11 with A B; Cong. } assert (H : A = B) by (apply between_cong_2 with I Y; Col). treat_equalities; intuition. } } { elim (eq_dec_points Z I); intro HZI; treat_equalities; Col. assert (HCong3 : Cong I A I B) by (apply l4_17 with X Y; unfold Midpoint in *; spliter; Cong). assert (H := l7_20 I A B). elim H; try ColR; intro. treat_equalities; exfalso; auto. ColR. } Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar