proposition: Lemma conga_cop_onc6_os__eqc : forall A B C D O P O' P', OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> OnCircle A O' P' -> OnCircle B O' P' -> OnCircle D O' P' -> Coplanar A B D O' -> OS A B C D -> CongA A C B A D B -> EqC O P O' P'.
proof: Proof. intros A B C D O P O' P' HA HB HC HCop HA' HB' HD' HCop' HOS HConga. apply eqc_chara. assert (O = O'); [|split; trivial; subst O'; apply cong_transitivity with O A; Cong]. assert (HNCol : ~ Col A B C) by (apply one_side_not_col123 with D, HOS). assert (HCong := onc2__cong O P). assert (HCong' := onc2__cong O' P'). destruct (col_dec A B O) as [|HNCol1]. { suma.assert_diffs. assert (Midpoint O A B) by (apply col_onc2__mid with P; assumption). apply (l7_17 A B); trivial. apply thales_converse_theorem_1 with D; auto. apply (l11_17 A C B); trivial. apply thales_theorem with O; auto. } assert (HNCol' : ~ Col A B D) by (apply one_side_not_col124 with C, HOS). destruct (midpoint_existence A B) as [M HM]. assert (HOS1 : OS A B O O'). { suma.assert_diffs; destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto. - apply one_side_transitivity with C; [|apply one_side_transitivity with D; trivial; apply one_side_symmetry]. apply acute_cop_onc3__os with P; auto. apply acute_cop_onc3__os with P'; auto. apply (acute_conga__acute A C B); assumption. - exfalso. apply HNCol1, col_permutation_1, midpoint_col. apply thales_converse_theorem_1 with C; auto. - exists C; split; [|apply l9_2, l9_8_2 with D; [apply l9_2|Side]]. apply cop_obtuse_onc3__ts with P; auto. apply cop_obtuse_onc3__ts with P'; auto. apply (conga_obtuse__obtuse A C B); assumption. } assert (HNCol1' : ~ Col A B O') by (apply one_side_not_col124 with O, HOS1). destruct (bet_cop_onc2__ex_onc_os_out O P A B C M) as [C1]; Between; Col; [suma.assert_diffs; auto..|]. destruct (bet_cop_onc2__ex_onc_os_out O' P' A B D M) as [D1]; Between; Col; [suma.assert_diffs; auto..|]. spliter. assert (HNCol2 : ~ Col A B C1) by (apply one_side_not_col124 with C; assumption). assert (HOut : Out M C1 D1). { apply (l9_19 A B); [Col| | apply one_side_transitivity with C; [|apply one_side_transitivity with D]; Side]. assert (O <> M) by (intro; subst; apply HNCol1; Col). assert (O' <> M) by (intro; subst; apply HNCol1'; Col). assert (Col O O' M); [|ColR]. suma.assert_diffs; apply (cop_per2__col A); auto; [|apply mid_onc2__per with P B; auto|apply mid_onc2__per with P' B; auto]. apply coplanar_trans_1 with B; Col; [|Cop]. apply coplanar_trans_1 with C; Col; [Cop|]. apply coplanar_perm_12, coplanar_trans_1 with D; Col; Cop. } destruct (eq_dec_points C1 D1). { subst D1. suma.assert_diffs. apply (cong4_cop2__eq A B C1); Cong; exists M; left; split; Col. } assert (HNCol2' : ~ Col A B D1) by (apply one_side_not_col124 with D; assumption). assert (CongA A C1 B A C B) by (apply (cop_onc4_os__conga O P); Side; exists M; left; split; Col). assert (CongA A D1 B A D B) by (apply (cop_onc4_os__conga O' P'); Side; exists M; left; split; Col). assert (Out A B M) by (suma.assert_diffs; apply l6_6, bet_out; Between). assert (Out B A M) by (suma.assert_diffs; apply l6_6, bet_out; Between). assert (HH := HOut). destruct HH as [HMC1 [HMD1 [HBet|HBet]]]; exfalso. - apply (lta_not_conga A D B A C B); CongA. apply (conga_preserves_lta A D1 B A C1 B); trivial. assert (Out D1 M C1) by (apply l6_6, bet_out; Between). apply os3__lta; [|apply one_side_symmetry, l9_19 with M; Col|]; apply one_side_transitivity with M. apply invert_one_side, out_one_side; Col. apply out_one_side; trivial; left; intro; apply HNCol2'; ColR. apply invert_one_side, out_one_side; Col. apply out_one_side; trivial; left; intro; apply HNCol2'; ColR. - apply (lta_not_conga A C B A D B); trivial. apply (conga_preserves_lta A C1 B A D1 B); trivial. assert (Out C1 M D1) by (apply l6_6, bet_out; Between). apply os3__lta; [|apply l9_19 with M; Col|]; apply one_side_transitivity with M. apply invert_one_side, out_one_side; Col. apply out_one_side; trivial; left; intro; apply HNCol2; ColR. apply invert_one_side, out_one_side; Col. apply out_one_side; trivial; left; intro; apply HNCol2; ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec