proposition: Lemma construction_uniqueness : forall A B D E, BetH A B D -> BetH A B E -> CongH B D B E -> D = E.
proof: Proof. intros A B D E HBet1 HBet2 HCong. assert (HD1 : A <> B) by (apply betH_expand in HBet1; spliter; auto). destruct (ncolH_exists _ _ HD1) as [C HNC]. assert (HConga : CongaH A C D A C E). { assert (HD2 := between_diff _ _ _ HBet1). assert (HD3 := between_diff _ _ _ HBet2). assert (HC1 := between_col _ _ _ HBet1). assert (HC2 := between_col _ _ _ HBet2). apply cong_5; try apply congH_refl; try apply addition_betH with B B; try apply congH_refl; auto; try (intro; subst; Col); try (apply HNC; ColHR). apply conga_out_conga with C B C B; try apply outH_trivial; try left; auto; try apply conga_refl; try intro; subst; apply HNC; Col. } assert (Hout : outH C D E). { assert (HD2 := between_diff _ _ _ HBet1). assert (HC := between_col _ _ _ HBet1). apply (cong_4_uniqueness A C D C D A D E); try apply conga_refl; try apply same_side_prime_refl; auto; try (intro; apply HNC; ColHR). destruct (between_out B A) as [F HBet3]; auto. split; [intro; subst; Col|intros l HI1 HI2; exists F; split]. { split; [intro; assert (ColH A C D) by (exists l; auto); apply HNC; ColHR|]. apply betH_expand in HBet3; spliter. split; [intro; assert (ColH A C F) by (exists l; auto); apply HNC; ColHR|]. exists A; split; trivial. apply betH_trans1 with B; Bet. } { apply betH_expand in HBet2; spliter. split; [intro; assert (ColH A C E) by (exists l; auto); apply HNC; ColHR|]. apply betH_expand in HBet3; spliter. split; [intro; assert (ColH A C F) by (exists l; auto); apply HNC; ColHR|]. exists A; split; trivial. apply betH_trans1 with B; Bet. } } apply betH_expand in HBet1; apply betH_expand in HBet2; apply outH_expand in Hout; spliter; apply inter_uniquenessH with A B C D; Col. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms