proposition: Lemma outH_dec : forall A B C, outH A B C \/ ~outH A B C.
proof: Proof. intros. assert(HH:=colH_dec A B C). induction HH. induction(eq_dec_pointsH A B). subst B. right. intro. unfold outH in H0. induction H0. apply betH_distincts in H0. tauto. induction H0. apply betH_distincts in H0. tauto. tauto. induction(eq_dec_pointsH A C). subst C. right. intro. unfold outH in H1. induction H1. apply betH_distincts in H1. tauto. induction H1. apply betH_distincts in H1. tauto. spliter. subst B. tauto. induction(eq_dec_pointsH B C). subst C. left. right; right. split; auto. apply between_one in H; auto. induction H. left. left; auto. induction H. left. right; left. Bet. right. intro. unfold outH in H3. induction H3. apply between_only_one' in H. tauto. induction H3. apply between_only_one' in H. tauto. apply betH_distincts in H. spliter. contradiction. right. intro. apply H. unfold outH in H0. induction H0. apply between_col in H0. tauto. induction H0. apply between_col in H0. spliter. Col. spliter. subst C. 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