proposition: Lemma bet_betCood_aux : forall O E S U1 U2 A AX AY B BX BY C CX CY, Cd O E S U1 U2 A AX AY -> Cd O E S U1 U2 B BX BY -> Cd O E S U1 U2 C CX CY -> Bet A B C -> Bet AX BX CX.
proof: Proof. intros O E S U1 U2 A AX AY B BX BY C CX CY HCdA HCdB HCdC HBet. destruct (parallel_existence S U1 A) as [A1 [A2 [HDiff4 [HPar HCol]]]]; try (intro; unfold Cd, Cs in *; spliter; treat_equalities; intuition). assert (HAX' := HCdA). destruct HAX' as [H [H' [HAX' H'']]]; clear H; clear H'; clear H''. destruct HAX' as [AX' [HProjpAX' HCongAX']]. assert (HA : Projp AX' A A1 A2). { split; auto; induction (eq_dec_points A AX'); [treat_equalities; right|left; split]; Col. apply par_perp__perp with S U1; auto. destruct HProjpAX' as [Hclear HAX']; clear Hclear. induction HAX'; spliter; Perp; intuition. } assert (HBX' := HCdB). destruct HBX' as [H [H' [HBX' H'']]]; clear H; clear H'; clear H''. destruct HBX' as [BX' [HProjpBX' HCongBX']]. destruct (exists_projp A1 A2 BX') as [BX'' HBX'']; auto. assert (HCX' := HCdC). destruct HCX' as [H [H' [HCX' H'']]]; clear H; clear H'; clear H''. destruct HCX' as [CX' [HProjpCX' HCongCX']]. destruct (exists_projp A1 A2 CX') as [CX'' HCX'']; auto. assert (HDiff : O <> E) by (unfold Cd, Cs in *; spliter; auto). assert (HColAX : Col O E AX). { unfold Cd in *; destruct HCdA as [H [H' [[PX [HProjp HCong]] H'']]]. apply projp_col in HProjp; apply l4_13 with S U1 PX; Cong. } assert (HColBX : Col O E BX). { unfold Cd in *; destruct HCdB as [H [H' [[PX [HProjp HCong]] H'']]]. apply projp_col in HProjp; apply l4_13 with S U1 PX; Cong. } assert (HColCX : Col O E CX). { unfold Cd in *; destruct HCdC as [H [H' [[PX [HProjp HCong]] H'']]]. apply projp_col in HProjp; apply l4_13 with S U1 PX; Cong. } apply l4_6 with AX' BX' CX'. { apply projp_preserves_bet with A B C S U1; auto. } { assert (Cong_5 O E AX BX CX S U1 AX' BX' CX') by (apply cong_3_3_cong_5; assert_diffs; auto). unfold Cong_5 in *; spliter; repeat (split; Cong). } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths