proposition: Lemma five_segment : forall A A' B B' C C' D D' : Point, Cong A B A' B' -> Cong B C B' C' -> Cong A D A' D' -> Cong B D B' D' -> Bet A B C -> Bet A' B' C' -> A <> B -> Cong C D C' D'.
proof: Proof. intros. unfold Bet in H3. decompose [or and] H3; clear H3. - unfold Bet in H4;decompose [or and] H4;clear H4. apply betH_expand in H6; apply betH_expand in H3;spliter. unfold Cong in *. decompose [or and] H; decompose [or and] H0; decompose [or and] H1; decompose [or and] H2; subst; auto using cong_permr, congH_permlr. clean_duplicated_hyps. clear H H0 H1 H2. destruct (eq_dec_pointsH C D). subst. right. split;auto. assert (CongH B' C' B' D'). apply cong_pseudo_transitivity with B D; auto. assert (BetH A' B' D'). apply cong_preserves_bet with A' B' C';auto using congH_refl. apply cong_pseudo_transitivity with A D;auto. apply addition with B B';auto using bet_disjoint. apply construction_uniqueness with A' B';try assumption. left. assert (C'<>D'). intro;subst. assert (CongH B D B C). apply cong_pseudo_transitivity with B' D'; apply congH_sym;auto. assert (BetH A B D). apply cong_preserves_bet with A' B' D';auto using congH_refl, congH_sym. apply H. apply construction_uniqueness with A B; auto using congH_sym, congH_refl. repeat split;auto. apply axiom_five_segmentsH with A A' B B';auto. left;split;auto. apply addition with B B'. Col. Col. apply bet_disjoint;apply between_comm;auto. apply bet_disjoint;apply between_comm;auto. apply congH_permlr;auto. apply congH_permlr;auto. contradiction. subst. exfalso;apply H5. apply cong_identity with B';auto. subst. assert (B=C). apply cong_identity with C';auto. subst;auto. - contradiction. - subst. assert (B'=C'). apply cong_identity with C. apply cong_sym;auto. subst. assumption. 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