proposition: Lemma segment_construction : forall A B C D, exists E, Bet A B E /\ Cong B E C D.
proof: Proof. intros. induction(eq_dec_pointsH C D). subst D. exists B. split. unfold Bet. tauto. unfold Cong. right; tauto. destruct (eq_dec_pointsH A B) as [HAB|HAB]. - subst. elim (other_point_exists B);intros A HBA. line B A l HBA. assert(HH:= cong_existence' C D l B H H0). ex_and HH F. ex_and H2 F'. apply betH_expand in H4. spliter. exists F. split. unfold Bet. auto. unfold Cong. repeat split;auto. - line A B l HAB. assert(HH:= cong_existence' C D l B H H1). ex_and HH F. ex_and H2 F'. apply betH_expand in H4. spliter. assert(ColH A F F'). line_col A F F'. induction(eq_dec_pointsH A F). subst F. exists F'. split. left; auto. left. repeat split; auto. induction (eq_dec_pointsH A F'). subst F'. exists F. split. left; Bet. left. repeat split; auto. apply between_one in H11; auto. induction H11. exists F'. split. assert(BetH B F A /\ BetH F' B A). apply betH_trans0; Bet. Bet. spliter. left. Bet. left. repeat split; auto. induction H11. exists F. assert(BetH B F' A /\ BetH F B A). apply betH_trans0; Bet. spliter. split. left. Bet. left. repeat split; auto. induction(eq_dec_pointsH A B). subst B. exists F. split. right; auto. left. repeat split; auto. assert(BetH F' A B \/ BetH F' B A). apply(betH2_out F' A B F); Bet. assert(BetH F A B \/ BetH F B A). apply(betH2_out F A B F'); Bet. induction H15. induction H16. assert(BetH A F F' \/ BetH A F' F). apply(out2_out B A F F' H9); Bet. induction H17; apply between_only_one' in H17. tauto. spliter. apply between_comm in H11. tauto. exists F. split. left. Bet. left. repeat split; auto. induction H16. exists F'. split. left. Bet. left. repeat split; auto. assert(BetH B F F' \/ BetH B F' F). apply(out2_out A B F F' H9); Bet. induction H17. apply between_only_one' in H17. tauto. apply between_only_one' in H17. spliter. apply between_comm in H4. tauto. 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