proposition: Lemma out_construction : forall A B X Y, X <> Y -> A <> B -> exists C, CongH A C X Y /\ (outH A B C).
proof: Proof. intros. line A B l H0. assert(HH:=cong_existence' X Y l A H H1). destruct HH as [P]. ex_and H3 P'. induction(outH_dec A B P). exists P. split; auto. exists P'. split; auto. line_col A B P'. apply betH_expand in H5. spliter. induction (eq_dec_pointsH B P'). subst P'. right; right. split; auto. apply between_one in H9; auto. induction H9. left. auto. induction H9. right; left. Bet. apply False_ind. induction(eq_dec_pointsH B P). subst P. apply H8. right; right; auto. apply H8. unfold outH. assert(BetH A B P \/ BetH A P B). apply(out2_out P' A B P); Bet. induction H16. left; auto. right; left; auto. 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